added entry for microwave example to readme and manifest

Signed-off-by: Konstantin Läufer <laufer@cs.luc.edu>

Author: klaeufer

README.md

@@ -143,6 +143,7 @@ Ideally these will be moved into this repo over time.
 | [Petri Nets](https://github.com/elh/petri-tlaplus)                                                                                | Instantiable Petri Nets with liveness properties                                                                                          | Eugene Huang                                                               |          |             |     ✔     |         |          |
 | [CRDT](https://github.com/JYwellin/CRDT-TLA)                                                                                      | Specifying and Verifying CRDT Protocols                                                                                                   | Ye Ji, Hengfeng Wei                                                        |          |             |     ✔     |         |          |
 | [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla)                                                                    | Consistency models provided by Azure Cosmos DB                                                                                            | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe            |          |             |     ✔     |    ✔    |          |
+| [Microwave](https://github.com/lucformalmethodscourse/microwave-tla)                                                                    | Simple microwave oven                                                                                            | Konstantin Läufer, George K. Thiruvathukal            |     ✔     |             |     ✔     |         |          |
 
 ## Contributing a Spec
 

manifest.json

@@ -5348,6 +5348,91 @@
           ]
         }
       ]
+    },
+    {
+      "path": "specifications/microwave",
+      "title": "Simple Microwave Oven"
+      "description": "Microwave oven with a very simple state space: door open or closed, heat on or off, zero or more seconds remaining.",
+      "sources": [
+        "https://ieeexplore.ieee.org/document/10754605"
+      ],
+      "authors": [
+        "Konstantin Läufer",
+        "George K. Thiruvathukal"
+      ],
+      "tags": [
+        "beginner"
+      ],
+      "modules": [
+        {
+          "path": "specifications/microwave/Microwave.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "features": [
+                "liveness"
+              ],
+              "mode": "exhaustive search",
+              "path": "specifications/microwave/Microwave.cfg",
+              "result": "success",
+              "runtime": "00:00:01",
+              "size": "small"
+            },
+            {
+              "features": [
+                "liveness"
+              ],
+              "mode": "exhaustive search",
+              "path": "specifications/microwave/MicrowaveChecked.cfg",
+              "result": "safety failure",
+              "runtime": "00:00:01",
+              "size": "small"
+            },
+            {
+              "features": [
+                "liveness"
+              ],
+              "mode": "exhaustive search",
+              "path": "specifications/microwave/MicrowaveChecked2.cfg",
+              "result": "safety failure",
+              "runtime": "00:00:01",
+              "size": "small"
+            },
+            {
+              "features": [
+                "liveness"
+              ],
+              "mode": "exhaustive search",
+              "path": "specifications/microwave/MicrowaveLive.cfg",
+              "result": "success",
+              "runtime": "00:00:01",
+              "size": "small"
+            },
+            {
+              "features": [
+                "liveness"
+              ],
+              "mode": "exhaustive search",
+              "path": "specifications/microwave/MicrowaveSafe.cfg",
+              "result": "success",
+              "runtime": "00:00:01",
+              "size": "small"
+            },
+            {
+              "features": [
+                "liveness"
+              ],
+              "mode": "exhaustive search",
+              "path": "specifications/microwave/MicrowaveStuttering.cfg",
+              "result": "liveness failure",
+              "runtime": "00:00:01",
+              "size": "small"
+            }
+          ]
+        }
+      ]
     }
   ]
-}
+}