[tlaplus] Re: making a sandwich: not sure how to terminate spec

Have you tried running your spec in TLC? Assuming that you can repeatedly make a sandwich there is no terminating condition required. However you will need some kind of fairness condition in your spec to ensure that once the sandwich is made (your MakeSandwich predicate) the jam and pb are eventually put back where they came from (your "Init" requirement). Perhaps someone more knowledgeable about TLA than me can comment on this but I'm not sure that the standard WF/SF constraints would cut it. The definition of WF_vars(A) is []ENABLED(A) ~> <A>_vars. However, none of your actions are forever enabled. It seems to me that what you want is ENABLED(A) ~> <A>_vars. The Specifying Systems book says that when an action once enabled can only be disabled by that action eventually occurring you can replace ENABLED(A) ~> <A>_vars with WF_vars(A) . But that doesn't seem to be the case here. And unfortunately, TLC won't accept constraints of the form ENABLED(A) ~> <A>_vars.

On Sunday, October 9, 2022 at 1:59:15 PM UTC-7 ben.is....@xxxxxxxxx wrote:

Hello,

I'm new to TLA+ and am working on a spec for making a sandwich to test my knowledge. I'm not clear how to indicate the sandwich is completed.

My draft spec is below, with explanation of what conditions I consider to be a completed sandwich. I'm not sure whether I should be using "eventually" or "leads_to" and how to construct a constraint that matches my model.

---- MODULE serial_sandwich ----

(***********************************************************************************)
(* inspired by *)
(* https://github.com/jameshfisher/tlaplus/blob/master/examples/DieHard/DieHard.tla *)

(***************************************************************************)
(* jam starts in fridge, *)
(* peanut butter (pb) in pantry, and bread is on table. *)
(* To construct the sandwich, gather all items on the table. *)
(* After sandwich is made, return items to their original location. *)

VARIABLES jam_location,
pb_location,
bread_location

(***************************************************************************)
(* valid locations for each of the *)
(* three items to be *)

TypeOk == /\ jam_location \in {"fridge", "table"}
/\ pb_location \in {"pantry", "table"}
/\ bread_location \in {"table"}

(***************************************************************************)
(* Define of the initial predicate -- *)
(* specifies the initial values of the variables. *)

Init == /\ jam_location = "fridge"
/\ pb_location = "pantry"
/\ bread_location = "table"

(***************************************************************************)
(* Define the actions *)

MoveJamToTable == /\ jam_location' = "table"
/\ pb_location' = pb_location
/\ bread_location' = bread_location

MoveJamToFridge == /\ jam_location' = "fridge"
/\ pb_location' = pb_location
/\ bread_location' = bread_location

MovePbToTable == /\ jam_location' = jam_location
/\ pb_location' = "table"
/\ bread_location' = bread_location

MovePbToPantry == /\ jam_location' = jam_location
/\ pb_location' = "pantry"
/\ bread_location' = bread_location

(***************************************************************************)
(* Define the next-state relation *)

Next == \/ MoveJamToTable
\/ MoveJamToFridge
\/ MovePbToTable
\/ MovePbToPantry

(***************************************************************************)
(* Define the formula Spec to be the complete specification, asserting *)
(* of a behavior that it begins in a state satisfying Init, and that every *)
(* step either satisfies Next or else leaves the set of locations unchanged *)

Spec == Init /\ [][Next]_<<jam_location,pb_location,bread_location>>

(***************************************************************************)
(* Successful sandwich will be completed when two conditions are met *)
(* 1) <<jam,pb,bread>> are all on table, *)
(* and then, sometime later *)
(* 2) <<jam,pb,bread>> are back to their initial locations. *)

MakeSandwich == /\ jam_location = "table"
/\ pb_location = "table"
/\ bread_location = "table"

(* I'm not clear how to express the terminating condition. *)
(* https://learntla.com/core/temporal-logic.html#eventually-diamond *)
(* https://learntla.com/core/temporal-logic.html#id2 *)

(* Done == MakeSandwich ~> Init *)

====

Kindly,

Ben Payne