21 Commits
Author SHA1 Message Date
Yury Gribov 916fe17f67 Assert that shim table is initialized. 2025-01-26 10:46:13 +03:00
Yury Gribov 4f6a055f72 Added todo. 2025-01-25 09:47:54 +03:00
Yury Gribov adb60eafb7 Mention lack of modules in Promela. 2025-01-25 09:47:02 +03:00
Yury Gribov ba5a586fe9 Simplify some EXCEPT directives. 2025-01-25 09:46:02 +03:00
Yury Gribov 8cd1b35ba1 Minor spec fixes. 2025-01-25 05:54:38 +03:00
Yury Gribov 006c9d7ac1 Print result in verification script. 2025-01-24 12:37:34 +03:00
Yury Gribov 5f533b4b55 Remove redundant semis. 2025-01-24 12:36:38 +03:00
Yury Gribov 0cdcf023c9 Learned how to use dedicated mtypes. 2025-01-24 12:30:50 +03:00
Yury Gribov 4235ef0330 Use new for-loops in model. 2025-01-24 12:23:13 +03:00
Yury Gribov a990595ff0 Added comment in spec. 2025-01-24 11:12:27 +03:00
Yury Gribov 96879fd0a2 Rename variable. 2025-01-24 11:12:27 +03:00
Yury Gribov 2b5d299b7c More automated verification driver. 2025-01-24 11:12:27 +03:00
Yury Gribov f0af663cd0 Minor Promela updates. 2025-01-24 11:12:27 +03:00
Yury Gribov ad6a00dfd1 Added todo. 2025-01-24 11:12:27 +03:00
Yury Gribov e08d19166b Added complaints about Promela. 2025-01-24 11:12:27 +03:00
Yury Gribov 6b9e17be61 Get rid of widths in Promela model. 2025-01-24 11:12:27 +03:00
Yury Gribov 388275accd Added Promela initialization model. 2025-01-24 11:12:27 +03:00
Yury Gribov 40ed720be0 Minor fixes in TLA spec. 2025-01-24 11:12:27 +03:00
Yury Gribov 0f5fc968ff Update spec README. 2025-01-24 11:12:27 +03:00
Yury Gribov 7218f80ef5 Minor spec fix. 2025-01-24 11:12:27 +03:00
Yury Gribov ea992cb0ae Added simple TLA+ model of Implib.so initialization code. 2025-01-24 11:12:27 +03:00