new examples for SAT, SMT, and Alloy

se-buw · Sep 10, 2024 · 67b14b7 · 67b14b7
1 parent d2ab7ee
commit 67b14b7
Showing 1 changed file with 25 additions and 21 deletions.
diff --git a/frontend/src/assets/config/Guides.json b/frontend/src/assets/config/Guides.json
@@ -1,5 +1,13 @@
 {
   "limboole": [
+    {
+      "title": "Validity Example",
+      "link": "https://play.formal-methods.net/?check=VAL&p=fringe-lapdog-scale-among"
+    },
+    {
+      "title": "Satisfiability Example",
+      "link": "https://play.formal-methods.net/?check=SAT&p=sloped-chair-yeast-vowed"
+    },
     {
       "title": "How to use limboole",
       "link": "https://raw.githubusercontent.com/maximaximal/limboole/master/README"
@@ -11,53 +19,49 @@
     {
       "title": "Lecture Slides on Moodle",
       "link": "https://moodle.uni-weimar.de/course/view.php?id=46635"
-    },
-    {
-      "title": "Validity Example",
-      "link": "https://play.formal-methods.net/?check=VAL&p=example-1"
-    },
-    {
-      "title": "Satisfiability Example",
-      "link": "https://play.formal-methods.net/?check=SAT&p=example-1"
     }
   ],
   "smt2": [
     {
-      "title": "SMTLIB Tutorial",
-      "link": "https://microsoft.github.io/z3guide/docs/logic/intro"
+      "title": "Example: Dog, Cat, Mouse",
+      "link": "https://play.formal-methods.net/?check=SMT&p=relock-clever-parcel-envy"
     },
     {
-      "title": "SMT-LIBv2",
-      "link": "https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf"
+      "title": "Example: Drinker's Paradox",
+      "link": "https://play.formal-methods.net/?check=SMT&p=unrest-viable-math-tall"
     },
     {
-      "title": "Example 1",
-      "link": "https://play.formal-methods.net/?check=SMT&p=example-1"
+      "title": "SMTLIB Tutorial",
+      "link": "https://microsoft.github.io/z3guide/docs/logic/intro"
     },
     {
-      "title": "Example 2",
-      "link": "https://play.formal-methods.net/?check=SMT&p=example-2"
+      "title": "SMT-LIBv2",
+      "link": "https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf"
     },
     {
       "title": "Lecture Slides on Moodle",
       "link": "https://moodle.uni-weimar.de/course/view.php?id=46635"
     }
   ],
   "xmv": [
+    {
+      "title": "Example: Traffic",
+      "link": "https://play.formal-methods.net/?check=XMV&p=example-1"
+    },
     {
       "title": "NuSMV 2.6 Tutorial",
       "link": "https://nusmv.fbk.eu/tutorial/v26/tutorial.pdf"
     },
     {
       "title": "NuSMV Manual",
       "link": "https://nusmv.fbk.eu/userman/v26/nusmv.pdf"
-    },
-    {
-      "title": "Example 1",
-      "link": "https://play.formal-methods.net/?check=XMV&p=example-1"
     }
   ],
   "als": [
+    {
+      "title": "Example: Traffic Light",
+      "link": "https://play.formal-methods.net/?check=ALS&p=bobble-payday-oboe-banana"
+    },
     {
       "title": "Alloy",
       "link": "https://alloytools.org/"
@@ -73,7 +77,7 @@
     {
       "title": "Tutorial for Alloy Analyzer 4.0",
       "link": "https://alloytools.org/tutorials/online/"
-    }
+    }    
   ],
   "spectra": [
     {