Skip to content

Commit

Permalink
Wei-jupiter-tla: +DoInt(c) in JupiterInterface, using DoInt(c) in Jup…
Browse files Browse the repository at this point in the history 
…iter protocols; see Issue #45
  • Loading branch information
hengxin committed Dec 31, 2018
1 parent ad7d44b commit 5c256a1
Show file tree
Hide file tree
Showing 174 changed files with 3,588 additions and 3,309 deletions.
Binary file modified tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.pdf
View file
Binary file not shown.
36 changes: 9 additions & 27 deletions tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,33 +33,16 @@ Init ==
/\ sbuf = [c \in Client |-> <<>>]
/\ srec = [c \in Client |-> 0]
-----------------------------------------------------------------------------
(*
Client c \in Client issues an operation op.
*)
DoOp(c, op) ==
/\ state' = [state EXCEPT ![c] = Apply(op, @)]
/\ cbuf' = [cbuf EXCEPT ![c] = Append(@, op)]
/\ crec' = [crec EXCEPT ![c] = 0]
/\ Comm(Msg)!CSend([c |-> c, ack |-> crec[c], op |-> op])

DoIns(c) ==
\E ins \in {op \in Ins: op.pos \in 1 .. (Len(state[c]) + 1) /\ op.ch \in chins /\ op.pr = Priority[c]}:
/\ DoOp(c, ins)
/\ chins' = chins \ {ins.ch}

DoDel(c) ==
\E del \in {op \in Del: op.pos \in 1 .. Len(state[c])}:
/\ DoOp(c, del)
/\ UNCHANGED chins

Do(c) ==
/\ \/ DoIns(c)
\/ DoDel(c)
/\ DoInt(DoOp, c)
/\ UNCHANGED <<sbuf, srec>>
-----------------------------------------------------------------------------
(*
Client c \in Client receives a message from the Server.
*)

Rev(c) ==
/\ Comm(Msg)!CRev(c)
/\ crec' = [crec EXCEPT ![c] = @ + 1]
Expand All @@ -70,11 +53,9 @@ Rev(c) ==
xcBuf == XformOpsOp(Xform, cShiftedBuf, m.op)
IN /\ cbuf' = [cbuf EXCEPT ![c] = xcBuf]
/\ state' = [state EXCEPT ![c] = Apply(xop, @)]
/\ UNCHANGED <<chins, sbuf, srec>>
-----------------------------------------------------------------------------
(*
The Server receives a message.
*)
/\ RevInt(c)
/\ UNCHANGED <<sbuf, srec>>

SRev ==
/\ Comm(Msg)!SRev
/\ LET m == Head(sincoming)
Expand All @@ -89,7 +70,8 @@ SRev ==
IF cl = c THEN xcBuf ELSE Append(sbuf[cl], xop)]
/\ state' = [state EXCEPT ![Server] = Apply(xop, @)]
/\ Comm(Msg)!SSend(c, [cl \in Client |-> [ack |-> srec[cl], op |-> xop]])
/\ UNCHANGED <<chins, cbuf, crec>>
/\ SRevInt
/\ UNCHANGED <<cbuf, crec>>
-----------------------------------------------------------------------------
Next ==
\/ \E c \in Client: Do(c) \/ Rev(c)
Expand All @@ -106,5 +88,5 @@ QC == \* Quiescent Consistency
THEOREM Spec => []QC
=============================================================================
\* Modification History
\* Last modified Sun Dec 30 16:02:35 CST 2018 by hengxin
\* Created Sat Jun 23 17:14:18 CST 2018 by hengxin
\* Last modified Mon Dec 31 21:02:17 CST 2018 by hengxin
\* Created Satchins, Jun 23 17:14:18 CST 2018 by hengxin
Binary file modified tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.toolbox/AJupiter.pdf
View file
Binary file not shown.
152 changes: 59 additions & 93 deletions tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.toolbox/AJupiter.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1031,159 +1031,125 @@
\@x{\makebox[0pt][r]{\scriptsize 34\hspace{1em}}\@s{16.4} \.{\land}
srec\@s{2.70} \.{=} [ c \.{\in} Client \.{\mapsto} 0 ]}%
\@x{\makebox[0pt][r]{\scriptsize 35\hspace{1em}}}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Client \ensuremath{c \.{\in} Client} issues an operation \ensuremath{op}.
\end{cpar}%
\end{lcom}%
\@x{\makebox[0pt][r]{\scriptsize 39\hspace{1em}} DoOp ( c ,\, op )
\@x{\makebox[0pt][r]{\scriptsize 36\hspace{1em}} DoOp ( c ,\, op )
\.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 40\hspace{1em}}\@s{26.06} \.{\land} state
\@x{\makebox[0pt][r]{\scriptsize 37\hspace{1em}}\@s{26.06} \.{\land} state
\.{'} \.{=} [ state {\EXCEPT} {\bang} [ c ] \.{=} Apply ( op ,\, @ ) ]}%
\@x{\makebox[0pt][r]{\scriptsize 41\hspace{1em}}\@s{26.06} \.{\land} cbuf
\@x{\makebox[0pt][r]{\scriptsize 38\hspace{1em}}\@s{26.06} \.{\land} cbuf
\.{'} \.{=} [ cbuf {\EXCEPT} {\bang} [ c ] \.{=} Append ( @ ,\, op ) ]}%
\@x{\makebox[0pt][r]{\scriptsize 42\hspace{1em}}\@s{26.06} \.{\land} crec
\@x{\makebox[0pt][r]{\scriptsize 39\hspace{1em}}\@s{26.06} \.{\land} crec
\.{'}\@s{2.19} \.{=} [ crec {\EXCEPT} {\bang} [ c ]\@s{2.19} \.{=} 0 ]}%
\@x{\makebox[0pt][r]{\scriptsize 43\hspace{1em}}\@s{26.06} \.{\land} Comm (
\@x{\makebox[0pt][r]{\scriptsize 40\hspace{1em}}\@s{26.06} \.{\land} Comm (
Msg ) {\bang} CSend ( [ c \.{\mapsto} c ,\, ack \.{\mapsto} crec [ c ] ,\,
op \.{\mapsto} op ] )}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 45\hspace{1em}} DoIns ( c ) \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 46\hspace{1em}}\@s{16.4} \E\, ins \.{\in} \{
op \.{\in} Ins \.{:} op . pos \.{\in} 1 \.{\dotdot} ( Len ( state [ c ] )
\.{+} 1 ) \.{\land} op . ch \.{\in} chins \.{\land} op . pr \.{=} Priority [
c ] \} \.{:}}%
\@x{\makebox[0pt][r]{\scriptsize 47\hspace{1em}}\@s{27.72} \.{\land} DoOp ( c
,\, ins )}%
\@x{\makebox[0pt][r]{\scriptsize 48\hspace{1em}}\@s{27.72} \.{\land} chins
\.{'} \.{=} chins \.{\,\backslash\,} \{ ins . ch \}}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 50\hspace{1em}} DoDel ( c ) \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 51\hspace{1em}}\@s{16.4} \E\, del \.{\in} \{
op \.{\in} Del \.{:} op . pos \.{\in} 1 \.{\dotdot} Len ( state [ c ] ) \}
\.{:}}%
\@x{\makebox[0pt][r]{\scriptsize 52\hspace{1em}}\@s{27.72} \.{\land} DoOp ( c
,\, del )}%
\@x{\makebox[0pt][r]{\scriptsize 53\hspace{1em}}\@s{27.72} \.{\land}
{\UNCHANGED} chins}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 55\hspace{1em}} Do ( c ) \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 56\hspace{1em}}\@s{22.34} \.{\land} \.{\lor}
DoIns ( c )}%
\@x{\makebox[0pt][r]{\scriptsize 57\hspace{1em}}\@s{33.45} \.{\lor} DoDel ( c
)}%
\@x{\makebox[0pt][r]{\scriptsize 58\hspace{1em}}\@s{22.34} \.{\land}
\@x{\makebox[0pt][r]{\scriptsize 42\hspace{1em}} Do ( c ) \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 43\hspace{1em}}\@s{22.34} \.{\land} DoInt (
DoOp ,\, c )}%
\@x{\makebox[0pt][r]{\scriptsize 44\hspace{1em}}\@s{22.34} \.{\land}
{\UNCHANGED} {\langle} sbuf ,\, srec {\rangle}}%
\@x{\makebox[0pt][r]{\scriptsize 59\hspace{1em}}}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
Client \ensuremath{c \.{\in} Client} receives a message from the
\ensuremath{Server}.
\end{cpar}%
\end{lcom}%
\@x{\makebox[0pt][r]{\scriptsize 63\hspace{1em}} Rev ( c ) \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 64\hspace{1em}}\@s{20.94} \.{\land} Comm (
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 46\hspace{1em}} Rev ( c ) \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 47\hspace{1em}}\@s{20.94} \.{\land} Comm (
Msg ) {\bang} CRev ( c )}%
\@x{\makebox[0pt][r]{\scriptsize 65\hspace{1em}}\@s{20.94} \.{\land} crec
\@x{\makebox[0pt][r]{\scriptsize 48\hspace{1em}}\@s{20.94} \.{\land} crec
\.{'} \.{=} [ crec {\EXCEPT} {\bang} [ c ] \.{=} @ \.{+} 1 ]}%
\@x{\makebox[0pt][r]{\scriptsize 66\hspace{1em}}\@s{20.94} \.{\land} \.{\LET}
\@x{\makebox[0pt][r]{\scriptsize 49\hspace{1em}}\@s{20.94} \.{\land} \.{\LET}
m \.{\defeq} Head ( cincoming [ c ] )}%
\@x{\makebox[0pt][r]{\scriptsize 67\hspace{1em}}\@s{52.45} cBuf \.{\defeq}
\@x{\makebox[0pt][r]{\scriptsize 50\hspace{1em}}\@s{52.45} cBuf \.{\defeq}
cbuf [ c ]}%
\@x{\makebox[0pt][r]{\scriptsize 68\hspace{1em}}\@s{52.45} cShiftedBuf
\@x{\makebox[0pt][r]{\scriptsize 51\hspace{1em}}\@s{52.45} cShiftedBuf
\.{\defeq} SubSeq ( cBuf ,\, m . ack \.{+} 1 ,\, Len ( cBuf ) )}%
\@x{\makebox[0pt][r]{\scriptsize 69\hspace{1em}}\@s{52.45} xop \.{\defeq}
\@x{\makebox[0pt][r]{\scriptsize 52\hspace{1em}}\@s{52.45} xop \.{\defeq}
XformOpOps ( Xform ,\, m . op ,\, cShiftedBuf )}%
\@x{\makebox[0pt][r]{\scriptsize 70\hspace{1em}}\@s{56.55} xcBuf \.{\defeq}
\@x{\makebox[0pt][r]{\scriptsize 53\hspace{1em}}\@s{56.55} xcBuf \.{\defeq}
XformOpsOp ( Xform ,\, cShiftedBuf ,\, m . op )}%
\@x{\makebox[0pt][r]{\scriptsize 71\hspace{1em}}\@s{36.15} \.{\IN} \.{\land}
\@x{\makebox[0pt][r]{\scriptsize 54\hspace{1em}}\@s{36.15} \.{\IN} \.{\land}
cbuf \.{'} \.{=} [ cbuf {\EXCEPT} {\bang} [ c ] \.{=} xcBuf ]}%
\@x{\makebox[0pt][r]{\scriptsize 72\hspace{1em}}\@s{56.55} \.{\land} state
\@x{\makebox[0pt][r]{\scriptsize 55\hspace{1em}}\@s{56.55} \.{\land} state
\.{'} \.{=} [ state {\EXCEPT} {\bang} [ c ] \.{=} Apply ( xop ,\, @ ) ]}%
\@x{\makebox[0pt][r]{\scriptsize 73\hspace{1em}}\@s{20.94} \.{\land}
{\UNCHANGED} {\langle} chins ,\, sbuf ,\, srec {\rangle}}%
\@x{\makebox[0pt][r]{\scriptsize 74\hspace{1em}}}\midbar\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
The \ensuremath{Server} receives a message.
\end{cpar}%
\end{lcom}%
\@x{\makebox[0pt][r]{\scriptsize 78\hspace{1em}} SRev \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 79\hspace{1em}}\@s{16.4} \.{\land} Comm (
\@x{\makebox[0pt][r]{\scriptsize 56\hspace{1em}}\@s{20.94} \.{\land} RevInt (
c )}%
\@x{\makebox[0pt][r]{\scriptsize 57\hspace{1em}}\@s{20.94} \.{\land}
{\UNCHANGED} {\langle} sbuf ,\, srec {\rangle}}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 59\hspace{1em}} SRev \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 60\hspace{1em}}\@s{16.4} \.{\land} Comm (
Msg ) {\bang} SRev}%
\@x{\makebox[0pt][r]{\scriptsize 80\hspace{1em}}\@s{16.4} \.{\land} \.{\LET}
\@x{\makebox[0pt][r]{\scriptsize 61\hspace{1em}}\@s{16.4} \.{\land} \.{\LET}
m \.{\defeq} Head ( sincoming )}%
\@x{\makebox[0pt][r]{\scriptsize 81\hspace{1em}}\@s{47.91} c\@s{3.77}
\@x{\makebox[0pt][r]{\scriptsize 62\hspace{1em}}\@s{47.91} c\@s{3.77}
\.{\defeq} m . c}%
\@x{\makebox[0pt][r]{\scriptsize 82\hspace{1em}}\@s{47.91} cBuf \.{\defeq}
\@x{\makebox[0pt][r]{\scriptsize 63\hspace{1em}}\@s{47.91} cBuf \.{\defeq}
sbuf [ c ]}%
\@x{\makebox[0pt][r]{\scriptsize 83\hspace{1em}}\@s{47.91} cShiftedBuf
\@x{\makebox[0pt][r]{\scriptsize 64\hspace{1em}}\@s{47.91} cShiftedBuf
\.{\defeq} SubSeq ( cBuf ,\, m . ack \.{+} 1 ,\, Len ( cBuf ) )}%
\@x{\makebox[0pt][r]{\scriptsize 84\hspace{1em}}\@s{47.91} xop \.{\defeq}
\@x{\makebox[0pt][r]{\scriptsize 65\hspace{1em}}\@s{47.91} xop \.{\defeq}
XformOpOps ( Xform ,\, m . op ,\, cShiftedBuf )}%
\@x{\makebox[0pt][r]{\scriptsize 85\hspace{1em}}\@s{52.01} xcBuf \.{\defeq}
\@x{\makebox[0pt][r]{\scriptsize 66\hspace{1em}}\@s{52.01} xcBuf \.{\defeq}
XformOpsOp ( Xform ,\, cShiftedBuf ,\, m . op )}%
\@x{\makebox[0pt][r]{\scriptsize 86\hspace{1em}}\@s{31.61} \.{\IN} \.{\land}
\@x{\makebox[0pt][r]{\scriptsize 67\hspace{1em}}\@s{31.61} \.{\IN} \.{\land}
srec \.{'}\@s{2.19} \.{=} [ cl \.{\in} Client \.{\mapsto}}%
\@x{\makebox[0pt][r]{\scriptsize 87\hspace{1em}}\@s{117.66} {\IF} cl \.{=} c
\@x{\makebox[0pt][r]{\scriptsize 68\hspace{1em}}\@s{117.66} {\IF} cl \.{=} c
\.{\THEN} srec [ cl ] \.{+} 1 \.{\ELSE} 0 ]}%
\@x{\makebox[0pt][r]{\scriptsize 88\hspace{1em}}\@s{52.01} \.{\land} sbuf
\@x{\makebox[0pt][r]{\scriptsize 69\hspace{1em}}\@s{52.01} \.{\land} sbuf
\.{'} \.{=} [ cl \.{\in} Client \.{\mapsto}}%
\@x{\makebox[0pt][r]{\scriptsize 89\hspace{1em}}\@s{117.66} {\IF} cl \.{=} c
\@x{\makebox[0pt][r]{\scriptsize 70\hspace{1em}}\@s{117.66} {\IF} cl \.{=} c
\.{\THEN} xcBuf \.{\ELSE} Append ( sbuf [ cl ] ,\, xop ) ]}%
\@x{\makebox[0pt][r]{\scriptsize 90\hspace{1em}}\@s{52.01} \.{\land} state
\@x{\makebox[0pt][r]{\scriptsize 71\hspace{1em}}\@s{52.01} \.{\land} state
\.{'} \.{=} [ state {\EXCEPT} {\bang} [ Server ] \.{=} Apply ( xop ,\, @ )
]}%
\@x{\makebox[0pt][r]{\scriptsize 91\hspace{1em}}\@s{52.01} \.{\land} Comm (
\@x{\makebox[0pt][r]{\scriptsize 72\hspace{1em}}\@s{52.01} \.{\land} Comm (
Msg ) {\bang} SSend ( c ,\, [ cl \.{\in} Client \.{\mapsto} [ ack
\.{\mapsto} srec [ cl ] ,\, op \.{\mapsto} xop ] ] )}%
\@x{\makebox[0pt][r]{\scriptsize 92\hspace{1em}}\@s{16.4} \.{\land}
{\UNCHANGED} {\langle} chins ,\, cbuf ,\, crec {\rangle}}%
\@x{\makebox[0pt][r]{\scriptsize 93\hspace{1em}}}\midbar\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 94\hspace{1em}} Next \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 95\hspace{1em}}\@s{16.4} \.{\lor} \E\, c
\@x{\makebox[0pt][r]{\scriptsize 73\hspace{1em}}\@s{16.4} \.{\land} SRevInt}%
\@x{\makebox[0pt][r]{\scriptsize 74\hspace{1em}}\@s{16.4} \.{\land}
{\UNCHANGED} {\langle} cbuf ,\, crec {\rangle}}%
\@x{\makebox[0pt][r]{\scriptsize 75\hspace{1em}}}\midbar\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 76\hspace{1em}} Next \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 77\hspace{1em}}\@s{16.4} \.{\lor} \E\, c
\.{\in} Client \.{:} Do ( c ) \.{\lor} Rev ( c )}%
\@x{\makebox[0pt][r]{\scriptsize 96\hspace{1em}}\@s{16.4} \.{\lor} SRev}%
\@x{\makebox[0pt][r]{\scriptsize 78\hspace{1em}}\@s{16.4} \.{\lor} SRev}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 98\hspace{1em}} Fairness \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 80\hspace{1em}} Fairness \.{\defeq}}%
\@y{\@s{0}%
There is no requirement that the clients ever generate operations.
}%
\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 99\hspace{1em}}\@s{16.4} {\WF}_{ vars} (
\@x{\makebox[0pt][r]{\scriptsize 81\hspace{1em}}\@s{16.4} {\WF}_{ vars} (
SRev \.{\lor} \E\, c \.{\in} Client \.{:} Rev ( c ) )}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 101\hspace{1em}} Spec \.{\defeq} Init
\@x{\makebox[0pt][r]{\scriptsize 83\hspace{1em}} Spec \.{\defeq} Init
\.{\land} {\Box} [ Next ]_{ vars}}%
\@y{\@s{0}%
\ensuremath{\.{\land} Fairness
}}%
\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 102\hspace{1em}}}\midbar\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 103\hspace{1em}} QC \.{\defeq}}%
\@x{\makebox[0pt][r]{\scriptsize 84\hspace{1em}}}\midbar\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 85\hspace{1em}} QC \.{\defeq}}%
\@y{\@s{0}%
Quiescent Consistency
}%
\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 104\hspace{1em}}\@s{20.37} Comm ( Msg )
\@x{\makebox[0pt][r]{\scriptsize 86\hspace{1em}}\@s{20.37} Comm ( Msg )
{\bang} EmptyChannel \.{\implies} Cardinality ( Range ( state ) ) \.{=} 1}%
\@pvspace{8.0pt}%
\@x{\makebox[0pt][r]{\scriptsize 106\hspace{1em}} {\THEOREM} Spec
\.{\implies} {\Box} QC}%
\@x{\makebox[0pt][r]{\scriptsize 107\hspace{1em}}}\bottombar\@xx{}%
\@x{\makebox[0pt][r]{\scriptsize 88\hspace{1em}} {\THEOREM} Spec \.{\implies}
{\Box} QC}%
\@x{\makebox[0pt][r]{\scriptsize 89\hspace{1em}}}\bottombar\@xx{}%
\setboolean{shading}{false}
\begin{lcom}{0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{\,\backslash\,}}* Modification History
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{\,\backslash\,}}* Last modified Sun \ensuremath{Dec} 30
16:02:35 \ensuremath{CST} 2018 by \ensuremath{hengxin
\ensuremath{\.{\,\backslash\,}}* Last modified \ensuremath{Mon}
\ensuremath{Dec} 31 21:02:17 \ensuremath{CST} 2018 by \ensuremath{hengxin
}%
\end{cpar}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\ensuremath{\.{\,\backslash\,}}* Created Sat \ensuremath{Jun} 23 17:14:18
\ensuremath{CST} 2018 by \ensuremath{hengxin
\ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Satchins}, Jun 23
17:14:18 \ensuremath{CST} 2018 by \ensuremath{hengxin
}%
\end{cpar}%
\end{lcom}%
Expand Down
4 changes: 2 additions & 2 deletions tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.toolbox/AJupiter___QC.launch
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="192.168.1.103"/>
<stringAttribute key="distributedNetworkInterface" value="114.212.83.69"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
Expand All @@ -20,7 +20,7 @@
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="crec, chins, cbuf, sincoming, state, cincoming, srec, sbuf"/>
<stringAttribute key="modelComments" value=""/>
<stringAttribute key="modelComments" value="(26877, 12409)"/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1QC"/>
Expand Down
Loading

0 comments on commit 5c256a1

Please sign in to comment.