nusmv villages

villages.smv

MODULE main 
VAR
    truck : 0..320;
    location :      { a, b, s,c };
    nextLocation :  { a, b, s,c};
    stockAtA : -1..120;
    stockAtB : -1..120;
    stockAtC : -1..200;

DEFINE 

    -- force 'taken' to be within the valid range
    takenA := stockAtA < 0 ? 0 : min(truck, 120 - stockAtA + cost);
    takenB := stockAtB < 0 ? 0 : min(truck, 120 - stockAtB + cost);
    takenC := stockAtC < 0 ? 0 : min(truck, 200 - stockAtC + cost);

    -- current value, subtract cost, fill to limit
    nextA := stockAtA + (toint(location = a) * takenA) - cost;
    nextB := stockAtB + (toint(location = b) * takenB) - cost;
    nextC := stockAtC + (toint(location = c) * takenC) - cost;

    taken := 
        case
             location = a: takenA; 
             location = b: takenB;
             location = c: takenC;
             TRUE: 0;
        esac;

    nextNextLocation := 
        case
            nextLocation = s: { a, b };
            nextLocation = a: { b, s, c };
            nextLocation = b: { a, s, c };
            nextLocation = c: { a, b };
        esac;

    cost := 
        case 
            location = a & nextLocation = b | location = b & nextLocation = a : 17;
            location = a & nextLocation = s | location = s & nextLocation = a : 29;
            location = a & nextLocation = c | location = c & nextLocation = a : 32;
            location = b & nextLocation = s | location = s & nextLocation = b : 21;
            location = b & nextLocation = c | location = c & nextLocation = b : 37;
            TRUE: 17;
        esac;

    nextTruck := 
        case
            location = s: 320;
            location = a: truck - takenA; 
            location = b: truck - takenB; 
            location = c: truck - takenC; 
        esac;

ASSIGN 
    -- INIT
    init(truck) := 320;
    init(location) := s;
    init(nextLocation) := b;
    init(stockAtA) := 40;
    init(stockAtB) := 30;
    init(stockAtC) := 145;

    -- NEXT

    next(truck) := nextTruck;
    next(location) := nextLocation;

    next(nextLocation) :=
        case
            nextLocation = s: { a, b };
            nextLocation = a: { b, s, c };
            nextLocation = b: { a, s, c };
            nextLocation = c: { a, b };
        esac;

    next(stockAtA) :=  
        case 
            nextA > 120 | nextA < 0: -1;
            TRUE: nextA;
        esac;

    next(stockAtB) :=  
        case 
            nextB > 120 | nextB < 0: -1;
            TRUE: nextB;
        esac;

    next(stockAtC) :=  
        case 
            nextC > 200 | nextC < 0: -1;
            TRUE: nextC;
        esac;


CTLSPEC EG (stockAtA >= 0 & stockAtB >= 0 & stockAtC >= 0)