Skip to content

K
KTLA Study
Commit 1584a247 authored by Kirill Smelkov's avatar Kirill Smelkov
Browse files
Options

.

parent e73c6cc7
Show whitespace changes
Inline Side-by-side
Showing with 3 additions and 3 deletions
MutualExclusionSpec.tla
View file @ 1584a247
...@@ -64,5 +64,5 @@ THEOREM Spec => Liveness ...@@ -64,5 +64,5 @@ THEOREM Spec => Liveness
============================================================================= =============================================================================
\* Modification History \* Modification History
\* Last modified Thu Feb 10 12:58:08 MSK 2022 by kirr \* Last modified Thu Feb 10 13:03:00 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr \* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1/MC.cfg
View file @ 1584a247
...@@ -5,7 +5,7 @@ p2 = p2 ...@@ -5,7 +5,7 @@ p2 = p2
\* MV CONSTANT definitions \* MV CONSTANT definitions
CONSTANT CONSTANT
Procs <- const_1644487333852943000 Procs <- const_1644487382552947000
\* SPECIFICATION definition \* SPECIFICATION definition
SPECIFICATION SPECIFICATION
Spec Spec
...@@ -16,4 +16,4 @@ MutualExclusion ...@@ -16,4 +16,4 @@ MutualExclusion
\* PROPERTY definition \* PROPERTY definition
PROPERTY PROPERTY
Liveness Liveness
\* Generated on Thu Feb 10 13:02:13 MSK 2022 \* Generated on Thu Feb 10 13:03:02 MSK 2022
\ No newline at end of file \ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment
GitLab Nexedi Edition | About GitLab | About Nexedi | 沪ICP备2021021310号-2 | 沪ICP备2021021310号-7