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;
+}
+