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 |
|