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

Hello again,

I made a few tweaks:

I replaced your a' = a with UNCHANGED. It's much easier to see which variables changed and which ones are UNCHANGED.
I added a fairness condition to Spec. /\ WF_vars(Next) this forces TLC to make some progress over the spec.
I added a count of sandwiches, a thing that actually gets made.
I added a Done condition, I don't know if this is right and I'd be happy to hear from the community if I could express this better

[](jam_location = "fridge" => <>(sandwiches > 0)) \* I think this means "Always, when there is jam in the "fridge" then eventually sandwiches is greater than 0.

Here's my model configuration:

In TLC options

add the following to TLC Command Line

-dump dot,actionlabels,colorize,snapshot sandwich.dot

This will make the following diagram so you can debug the state transitions.

Running this model, TLC finds a path that leads to not making a sandwich.

Jeremy

On Tue, Dec 6, 2022 at 12:08 PM Jeremy Wright <jeremy@xxxxxxxxxxxx> wrote:

Hello Ben,

I made a similar toy spec. You might find some useful bits there if you haven't see it already: https://youtu.be/zP-GJsdqq24

Jeremy

On Mon, Dec 5, 2022 at 1:59 PM ns <nedsri1988@xxxxxxxxx> wrote:
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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/640e9718-89a3-49c4-956f-b50837c69be2n%40googlegroups.com.

--
Jeremy