Merge branch 'master' of https://github.com/Barnard-PL-Labs/CYOA-TSL

Barnard-PL-Labs · Sep 25, 2023 · 27dbbfe · 27dbbfe
2 parents 08ef6cd + d19a66c
commit 27dbbfe
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 0 deletions.
diff --git a/spec engineering/CYOAxTSL.md → spec_engineering/CYOAxTSL.md b/spec engineering/CYOAxTSL.md → spec_engineering/CYOAxTSL.md
diff --git a/spec engineering/automaton.png → spec_engineering/automaton.png b/spec engineering/automaton.png → spec_engineering/automaton.png
diff --git a/spec_engineering/specV2.tsl 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;
+}
+