copilot-instructions.md

• Do not use temporal properties (PROPERTY or PROPERTIES) when modeling logic puzzles with TLA+. Instead, to find a solution using TLC, express the negation of the goal state as an ordinary safety property (INVARIANT).

• Do not write a PlusCal algorithm. Always write a TLA+ specification.

• The TLA+ module FiniteSetsExt provides a Min(S) and a Max(S) operator that can be used to get the minimum and maximum elements of a finite set S.

RiverCrossingFlashlight.cfg

SPECIFICATION Spec

CONSTANTS
    A = "A"
    B = "B"
    C = "C"
    D = "D"

INVARIANT NotGoal

\* When TLC finds a violation of NotGoal, it means we've found a solution

RiverCrossingFlashlight.prompt.md

mode	tools
agent	tlaplus_check tlaplus_parse tlaplus_symbol

Formalize the following problem using TLA+. Use TLC to find the solution.

4 people, a bridge and a flashlight problem

Four people need to cross a bridge at night. The bridge is only strong enough to hold at most two people at once. Because it is night a flashlight must be used for all crossings. It takes person A ten minutes to cross, person B five minutes, person C two minutes, and person D one minute. If two cross at the same time they must walk at the slower man's pace. How can you get everyone across in 17 minutes?

RiverCrossingFlashlight.tla

-------------------------------- MODULE RiverCrossingFlashlight --------------------------------
EXTENDS Naturals, FiniteSets, FiniteSetsExt, Sequences

CONSTANTS A, B, C, D

\* Crossing times for each person
Times(p) == CASE p = A -> 10
              [] p = B -> 5
              [] p = C -> 2
              [] p = D -> 1
              [] OTHER -> 0

\* Left and right sides of the bridge
Left == "left"
Right == "right"

VARIABLES 
    people,    \* Set of people on the left side
    flashlight, \* Position of the flashlight (Left or Right)
    elapsedTime, \* Total time elapsed
    solution   \* Sequence of moves made

\* Initial state has everyone on the left with the flashlight
Init ==
    /\ people = {A, B, C, D}
    /\ flashlight = Left
    /\ elapsedTime = 0
    /\ solution = << >>

\* Helper function to find crossing time when multiple people cross
CrossingTime(group) == 
    IF Cardinality(group) = 0 THEN 0
    ELSE Max({Times(p) : p \in group})

\* People can cross from left to right
CrossLeftToRight ==
    /\ flashlight = Left
    /\ \E group \in SUBSET people :
        /\ group # {}
        /\ Cardinality(group) \in {1, 2}
        /\ people' = people \ group
        /\ flashlight' = Right
        /\ elapsedTime' = elapsedTime + CrossingTime(group)
        /\ solution' = solution \o <<[direction |-> "LEFT_TO_RIGHT", group |-> group, time |-> CrossingTime(group)]>>

\* People can cross from right to left
CrossRightToLeft ==
    /\ flashlight = Right
    /\ \E group \in SUBSET ({A, B, C, D} \ people) :
        /\ group # {}
        /\ Cardinality(group) \in {1, 2}
        /\ people' = people \union group
        /\ flashlight' = Left
        /\ elapsedTime' = elapsedTime + CrossingTime(group)
        /\ solution' = solution \o <<[direction |-> "RIGHT_TO_LEFT", group |-> group, time |-> CrossingTime(group)]>>

\* Next state is either crossing left to right or right to left
Next ==
    \/ CrossLeftToRight
    \/ CrossRightToLeft

\* Variables that change in the spec
vars == <<people, flashlight, elapsedTime, solution>>

\* The type invariant
TypeInvariant ==
    /\ people \subseteq {A, B, C, D}
    /\ flashlight \in {Left, Right}
    /\ elapsedTime \in Nat

\* Goal: Everyone is across the bridge
Goal ==
    /\ people = {}
    /\ flashlight = Right
    /\ elapsedTime <= 17

\* We will use this invariant to find a solution by negating the goal
NotGoal == ~Goal

\* The specification
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

=============================================================================
\* Modification History
\* Created by TLA+ modeling