gistfile1.tla

---- MODULE refueling ----
EXTENDS TLC, Integers, Naturals, FiniteSets
VARIABLES position, fuel, numberOfStops, stations

vars == <<position, fuel, numberOfStops, stations>>

Range(f) == {f[x]: x \in DOMAIN f}
Max(S) == CHOOSE i \in S : \A j \in S : i >= j
Min(S) == CHOOSE i \in S : \A j \in S : i <= j
Abs(x) == Max({x, -x})
Distance(pos1, pos2) == Abs(pos1 - pos2)
EmptyStation(pos) == [stations EXCEPT ![pos] = 0]


\* target == 1
\* startFuel == {1}
\* startStations == {(0 :> 0)}

\* target == 100
\* startFuel == {1}
\* startStations == {(10 :> 100)}

\* target == 100
\* startFuel == {10}
\* startStations == {(
\*   10 :> 60 @@
\*   20 :> 30 @@
\*   30 :> 30 @@
\*   60 :> 40
\* )}

distanceRange == 1..10
target == Max(distanceRange)
maxStations == 2
stationPositions == {s \in SUBSET distanceRange: Cardinality(s) <= maxStations}
startStations == UNION {[Dom -> distanceRange]:  Dom \in stationPositions}
\* startFuel == {f \in distanceRange: f < target /\ f >= Min(DOMAIN startStations)}
startFuel == distanceRange


Init ==
  /\ position = 0
  /\ numberOfStops = 0
  /\ stations \in startStations
  /\ fuel \in startFuel

Next ==
  \/
    /\ target /= position
    /\
      IF Distance(position, target) <= fuel THEN
        /\ position' = target
        /\ fuel' = fuel - Distance(position, target)
        \* /\ numberOfStops' = numberOfStops + 1
        /\ UNCHANGED <<stations, numberOfStops>>
      ELSE \E nextPosition \in DOMAIN stations:
        LET distance == Distance(position, nextPosition) IN
        /\ distance <= fuel
        /\ fuel' =  (fuel - distance) + stations[nextPosition]
        /\ stations' = EmptyStation(nextPosition)
        /\ numberOfStops' = numberOfStops + 1
        /\ position' = nextPosition
  \/ UNCHANGED vars

Spec == Init /\ [][Next]_vars

-------------------------------------------------------------
-------------------------------------------------------------
TargetNotReached == target /= position
StationsTypeInvariant ==
  /\ \A pos \in DOMAIN stations: pos \in Nat
  /\ \A stationFuel \in Range(stations): stationFuel \in Nat

TypeInvariant ==
  /\ StationsTypeInvariant
  /\ fuel \in Nat
  /\ numberOfStops \in Nat
  /\ position \in Nat

numberOfStopsIncreases == numberOfStops' >= numberOfStops

====