From d19a66c2eb157057ac2733386bd6617731a55ebd Mon Sep 17 00:00:00 2001
From: Mark Santolucito <mark.santolucito@yale.edu>
Date: Sun, 24 Sep 2023 18:34:31 -0400
Subject: [PATCH] add a new version of the spec

also seems like the tsl-api is out of date with the command liner version - still should be correct i think, but the command line version sometimes gives smaller solutions
---
 .../CYOAxTSL.md                               |   0
 .../automaton.png                             | Bin
 spec_engineering/specV2.tsl                   |  28 ++++++++++++++++++
 3 files changed, 28 insertions(+)
 rename {spec engineering => spec_engineering}/CYOAxTSL.md (100%)
 rename {spec engineering => spec_engineering}/automaton.png (100%)
 create mode 100644 spec_engineering/specV2.tsl

diff --git a/spec engineering/CYOAxTSL.md b/spec_engineering/CYOAxTSL.md
similarity index 100%
rename from spec engineering/CYOAxTSL.md
rename to spec_engineering/CYOAxTSL.md
diff --git a/spec engineering/automaton.png b/spec_engineering/automaton.png
similarity index 100%
rename from spec engineering/automaton.png
rename to spec_engineering/automaton.png
diff --git a/spec_engineering/specV2.tsl b/spec_engineering/specV2.tsl
new file mode 100644
index 0000000..12ff6ef
--- /dev/null
+++ b/spec_engineering/specV2.tsl
@@ -0,0 +1,28 @@
+initially assume{
+    ! inCave passage;
+    ! inMarket passage;
+    ! inTown passage;    
+}
+
+always assume {
+//we wont hallucinate a cave, but we might accidentally end up in town or at a market
+    [passage <- toCave passage] <-> X inCave passage;
+    [passage <- toMarket passage] -> X inMarket passage;
+    [passage <- toTown passage] -> X inTown passage;
+}
+
+guarantee {
+//you cant go to the cave until you have been to town and the market once
+    (! (inCave passage)) W (inMarket passage);
+    (! (inCave passage)) W (inTown passage);
+
+}
+
+always guarantee {
+//eventually, always visit all the places, and keep summary up to date
+    [summary <- updateSummary passage];
+    F inCave passage;
+    F inMarket passage;
+    F inTown passage;
+}
+