-
Notifications
You must be signed in to change notification settings - Fork 0
Home
Kangfeng Ye edited this page Jul 11, 2016
·
8 revisions
Welcome to the Circus2ZCSP wiki!
Circus2ZCSP is a translator to link a Circus model to a CSP || Z model which is finally model-checked by ProB. Actually Z is translated into internal B by ProZ, a translator from Z to B in ProB. So eventually it is a CSP || B model. The theory behind is published in this paper: Model checking of state-rich formalism Circus by linking to CSP || B
-
$ java -jar circus2zcsp-ass-20160630.jarusage: java -jar circus2zcsp.jar spec.tex [spec1.tex [...]] [-d] [-v] [-V] Circus2ZCSP is a translator to link one (or more) Circus specification to its corresponding model in Z || CSP, which is sequentially model-checked by ProB. Options: -d,--verbose run in debug mode -v,--version show version -V,--Versions show detailed versions information For any problems, please contac <[email protected]> or <[email protected]> -
$ java -jar circus2zcsp-ass-20160630.jar -vCurrent Circus2ZCSP version: 0.3 -
$ java -jar circus2zcsp-ass-20160630.jar -VCurrent Circus2ZCSP version: 0.3 ==> 0.1 This is the first release built on March 15th, 2016. It is capable of translating all constructs in the reactive buffer and the steam boiler cases. Limitations: 1. External choice of actions are only available to "prefixed" actions (such as basic actions, prefixing, guarded commands), and compound CSP actions of the se "prefixed" actions. 2. Parallel composition and interleaving for actions are not supported if bo th actions share variables in scope. 3. Operator template is not supported. 4. Reflexive-transitive closure (*) is not supported. ==> 0.2 This is the second release built on May 13th, 2016. It is capable of translating all constructs in the reactive buffer, the steam boiler cases, and the ESEL cas e. -------------------------------------- New ------------------------------------ 1. Add support of iterated parallel and interleaving of actions for the case if their actions have disjoint variables in scope 2. Add support of iterated parallel of processes ------------------------------------- Fixed ----------------------------------- 1. Add parenthesis around translated freetype constructor d~1: d.1 => (d.1) in c sp 2. The problem that freetype is not translated to CSP though this type is used i n the behavioural part ------------------------------------ Changed ---------------------------------- 1. The processing of u'=u (u - variables not in frame) in schema expression as a ction 1.1 if v' is included in its declaration part, then this v is regarded in fr ame 1.2 if v' is nto included in its declaration part (though v might be include d), then this v is regarded not in frame 2. The logic to include parent sections 2.1 use a stack to keep dependency order of all sections 2.2 assemble all sections into a big section according to their dependency o rder ----------------------------------- Limitations ------------------------------- 1. External choice of actions are only available to "prefixed" actions (such as basic actions, prefixing, guarded commands), and compound CSP actions of these " prefixed" actions. 2. Parallel composition and interleaving for actions are not supported if both a ctions share variables in scope. 3. Operator template is not supported. 4. Reflexive-transitive closure (*) is not supported. ==> 0.3 This is the third release built on June 30th, 2016. It is capable of translating all constructs in the reactive buffer, the steam boiler cases, and the ESEL cas e. -------------------------------------- New ------------------------------------ ------------------------------------- Fixed ----------------------------------- ------------------------------------ Changed ---------------------------------- 1. Check if a schema that corresponding a schema expression as action shall be an operational schema. ----------------------------------- Limitations ------------------------------- 1. External choice of actions are only available to "prefixed" actions (such as basic actions, prefixing, guarded commands), and compound CSP actions of these " prefixed" actions. 2. Parallel composition and interleaving for actions are not supported if both a ctions share variables in scope. 3. Operator template is not supported. 4. Reflexive-transitive closure (*) is not supported. -
translate a specification:
$ java -jar circus2zcsp-ass-20160630.jar buffer_spec.tex -
translate a specification with debug mode:
$ java -jar circus2zcsp-ass-20160630.jar -d buffer_spec.tex[DEBUG] Reading spec: buffer_spec.tex [DEBUG] czt.path is set to '/Users/ykf_2001/Downloads/circus2csp_jar_process/buffer_spec' Jul 11, 2016 10:19:52 PM net.sourceforge.czt.z.util.WarningManager doWarn WARNING: Schema expression action still requires StateUpdate in process signature. Process...: Buffer Action....: Input Jul 11, 2016 10:19:52 PM net.sourceforge.czt.z.util.WarningManager doWarn WARNING: Schema expression action still requires StateUpdate in process signature. Process...: Buffer Action....: Output Jul 11, 2016 10:19:52 PM net.sourceforge.czt.z.util.WarningManager doWarn WARNING: Schema expression action still requires StateUpdate in process signature. Process...: Buffer Action....: $$mainAction\_ L26C5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_BufferInit] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_InputCmd] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 x?,ℕ [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_OutputCmd] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_OP_buff] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff!,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_OP_size] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size!,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_BufferInit_fOp] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_InputCmd_fOp] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 x?,ℕ [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 5 [DEBUG] StateMergeOmega1.java:isOperationalSchema:408 =============== isOperationalSchema [Buffer_OutputCmd_fOp] ===================== [DEBUG] StateMergeOmega1.java:isOperationalSchema:413 Variables found: 4 [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size′,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_buff′,RefExpr(seq _ [ℕ]_E_) [DEBUG] StateMergeOmega1.java:isOperationalSchema:419 Buffer_size,ApplExpr{LHS= _ .. _ , RHS=TupleExpr(0, maxbuff), MF=true} [DEBUG] StateMergeOmega1.java:isOperationalSchema:427 Variables added: 4 [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [maxbuff, null]: [] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [input, null]: [] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [output, null]: [] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_BufferState, Buffer]: [(maxbuff, null) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_BufferInit, Buffer]: [(maxbuff, null) (Buffer_BufferState, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_InputCmd, Buffer]: [(maxbuff, null) (Buffer_BufferState, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OutputCmd, Buffer]: [(Buffer_BufferState, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OP_buff, Buffer]: [(Buffer_BufferState, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OP_size, Buffer]: [(maxbuff, null) (Buffer_BufferState, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_BufferInit_fOp, Buffer]: [(Buffer_BufferState, Buffer) (Buffer_BufferInit, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_InputCmd_fOp, Buffer]: [(Buffer_BufferState, Buffer) (Buffer_InputCmd, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OutputCmd_fOp, Buffer]: [(Buffer_BufferState, Buffer) (Buffer_OutputCmd, Buffer) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer, null]: [(maxbuff, null) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OP_size, null]: [(maxbuff, null) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OP_size, null]: [(maxbuff, null) ] [DEBUG] DefinitionReferencesMapVisitor.java:addToRefMap:249 Put [Buffer_OP_buff, null]: [] [DEBUG] Circus2ZCSPUtils.java:printRefMap:1968 ###################### [Start] Ref Map ##################### [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer, null)]: (maxbuff, null) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_BufferInit, Buffer)]: (maxbuff, null), (Buffer_BufferState, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_BufferInit_fOp, Buffer)]: (Buffer_BufferState, Buffer), (Buffer_BufferInit, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_BufferState, Buffer)]: (maxbuff, null) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_InputCmd, Buffer)]: (maxbuff, null), (Buffer_BufferState, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_InputCmd_fOp, Buffer)]: (Buffer_BufferState, Buffer), (Buffer_InputCmd, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_OP_buff, null)]: [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_OP_buff, Buffer)]: (Buffer_BufferState, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_OP_size, null)]: (maxbuff, null) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_OP_size, Buffer)]: (maxbuff, null), (Buffer_BufferState, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_OutputCmd, Buffer)]: (Buffer_BufferState, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(Buffer_OutputCmd_fOp, Buffer)]: (Buffer_BufferState, Buffer), (Buffer_OutputCmd, Buffer) [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(input, null)]: [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(maxbuff, null)]: [DEBUG] Circus2ZCSPUtils.java:printRefMap:1989 [(output, null)]: [DEBUG] Circus2ZCSPUtils.java:printRefMap:1996 ###################### [End] Ref Map ##################### [DEBUG] Before sort [Buffer_buff′ Buffer_size′ Buffer_size Buffer_buff ] [DEBUG] After sort [Buffer_buff Buffer_buff′ Buffer_size Buffer_size′ ] [DEBUG] Before sort [Buffer_size Buffer_size′ Buffer_buff′ Buffer_buff x? ] [DEBUG] After sort [Buffer_buff Buffer_buff′ Buffer_size Buffer_size′ x? ] [DEBUG] Before sort [Buffer_buff Buffer_size Buffer_buff′ Buffer_size′ ] [DEBUG] After sort [Buffer_buff Buffer_buff′ Buffer_size Buffer_size′ ] [DEBUG] ================= [Start] Section [BufferSpec] =================== [DEBUG] ================= [Start] Z in ISO Z ====================== [DEBUG] \begin{zsection} \SECTION BufferSpec \parents~standard\_toolkit \end{zsection} \begin{axdef}maxbuff : \nat _{1} \where maxbuff = 2 \end{axdef} \begin{zed}Buffer\_ BufferState == [ Buffer\_ buff : \seq \nat ; Buffer\_ size : 0 \upto maxbuff | Buffer\_ size =~\# Buffer\_ buff \leq maxbuff ] \end{zed} \begin{zed}State == Buffer\_ BufferState \end{zed} \begin{zed}Init == [ State~' | Buffer\_ buff' =~\langle \rangle \land Buffer\_ size' = 0 ] \end{zed} \begin{zed}Buffer\_ BufferInit == [ ( Buffer\_ BufferState ) ' ; Buffer\_ size : 0 \upto maxbuff ; Buffer\_ buff : \seq \nat | Buffer\_ buff' =~\langle \rangle \land Buffer\_ size' = 0 ] \end{zed} \begin{zed}Buffer\_ InputCmd == [ \Delta Buffer\_ BufferState ; x? : \nat | Buffer\_ size < maxbuff \land Buffer\_ buff' = Buffer\_ buff \cat \langle x? \rangle \land Buffer\_ size' = Buffer\_ size + 1 ] \end{zed} \begin{zed}Buffer\_ OutputCmd == [ \Delta Buffer\_ BufferState | Buffer\_ size > 0 \land Buffer\_ buff' = tail~Buffer\_ buff \land Buffer\_ size' = Buffer\_ size - 1 ] \end{zed} \begin{zed}Buffer\_ OP\_ buff == [ \Xi Buffer\_ BufferState ; Buffer\_ buff! : \seq \nat | Buffer\_ buff! = Buffer\_ buff ] \end{zed} \begin{zed}Buffer\_ OP\_ size == [ \Xi Buffer\_ BufferState ; Buffer\_ size! : 0 \upto maxbuff | Buffer\_ size! = Buffer\_ size ] \end{zed} \begin{zed}Buffer\_ BufferInit\_ fOp == [ \Xi Buffer\_ BufferState | \lnot \pre Buffer\_ BufferInit ] \end{zed} \begin{zed}Buffer\_ InputCmd\_ fOp == [ \Xi Buffer\_ BufferState ; x? : \nat | \lnot \pre Buffer\_ InputCmd ] \end{zed} \begin{zed}Buffer\_ OutputCmd\_ fOp == [ \Xi Buffer\_ BufferState | \lnot \pre Buffer\_ OutputCmd ] \end{zed} [DEBUG] ================= [End] Z in ISO Z ======================== [DEBUG] ================= [Start] Z in ISO Z ====================== [DEBUG] \begin{zsection} \SECTION BufferSpec \parents~standard\_toolkit \end{zsection} \begin{axdef}maxbuff : \nat _{1} \where maxbuff = 2 \end{axdef} \begin{zed}Buffer\_ BufferState == [ Buffer\_ buff : \seq \nat ; Buffer\_ size : 0 \upto maxbuff | Buffer\_ size =~\# Buffer\_ buff \leq maxbuff ] \end{zed} \begin{zed}State == Buffer\_ BufferState \end{zed} \begin{zed}Init == [ State~' | Buffer\_ buff' =~\langle \rangle \land Buffer\_ size' = 0 ] \end{zed} \begin{zed}Buffer\_ BufferInit == [ ( Buffer\_ BufferState ) ' ; Buffer\_ size : 0 \upto maxbuff ; Buffer\_ buff : \seq \nat | Buffer\_ buff' =~\langle \rangle \land Buffer\_ size' = 0 ] \end{zed} \begin{zed}Buffer\_ InputCmd == [ \Delta Buffer\_ BufferState ; x? : \nat | Buffer\_ size < maxbuff \land Buffer\_ buff' = Buffer\_ buff \cat \langle x? \rangle \land Buffer\_ size' = Buffer\_ size + 1 ] \end{zed} \begin{zed}Buffer\_ OutputCmd == [ \Delta Buffer\_ BufferState | Buffer\_ size > 0 \land Buffer\_ buff' = tail~Buffer\_ buff \land Buffer\_ size' = Buffer\_ size - 1 ] \end{zed} \begin{zed}Buffer\_ OP\_ buff == [ \Xi Buffer\_ BufferState ; Buffer\_ buff! : \seq \nat | Buffer\_ buff! = Buffer\_ buff ] \end{zed} \begin{zed}Buffer\_ OP\_ size == [ \Xi Buffer\_ BufferState ; Buffer\_ size! : 0 \upto maxbuff | Buffer\_ size! = Buffer\_ size ] \end{zed} \begin{zed}Buffer\_ BufferInit\_ fOp == [ \Xi Buffer\_ BufferState | \lnot \pre Buffer\_ BufferInit ] \end{zed} \begin{zed}Buffer\_ InputCmd\_ fOp == [ \Xi Buffer\_ BufferState ; x? : \nat | \lnot \pre Buffer\_ InputCmd ] \end{zed} \begin{zed}Buffer\_ OutputCmd\_ fOp == [ \Xi Buffer\_ BufferState | \lnot \pre Buffer\_ OutputCmd ] \end{zed} [DEBUG] ================= [End] Z in ISO Z ======================== [DEBUG] ================= [Start] Type Check ====================== [DEBUG] ================= [End] Type Check Done =================== [DEBUG] ================= [Start] Z in ZRM ======================== [DEBUG] \documentclass{article} \usepackage{fuzz} \begin{document} %\begin{zsection} \SECTION BufferSpec \parents~standard\_toolkit %\end{zsection} \begin{axdef} maxbuff : \nat_1 \where maxbuff = 2 \end{axdef} \begin{zed} Buffer\_BufferState \defs [~ Buffer\_buff : \seq \nat ; Buffer\_size : 0 \upto maxbuff | Buffer\_size =~\# Buffer\_buff \leq maxbuff ~] \end{zed} \begin{zed} State \defs Buffer\_BufferState \end{zed} \begin{zed} Init \defs [~ State' | Buffer\_buff' =~\langle \rangle \land Buffer\_size' = 0 ~] \end{zed} \begin{zed} Buffer\_BufferInit \defs [~ Buffer\_BufferState' ; Buffer\_size : 0 \upto maxbuff ; Buffer\_buff : \seq \nat | Buffer\_buff' =~\langle \rangle \land Buffer\_size' = 0 ~] \end{zed} \begin{zed} Buffer\_InputCmd \defs [~ \Delta Buffer\_BufferState ; x? : \nat | Buffer\_size < maxbuff \land Buffer\_buff' = Buffer\_buff \cat \langle x? \rangle \land Buffer\_size' = Buffer\_size + 1 ~] \end{zed} \begin{zed} Buffer\_OutputCmd \defs [~ \Delta Buffer\_BufferState | Buffer\_size > 0 \land Buffer\_buff' = tail~Buffer\_buff \land Buffer\_size' = Buffer\_size - 1 ~] \end{zed} \begin{zed} Buffer\_OP\_buff \defs [~ \Xi Buffer\_BufferState ; Buffer\_buff! : \seq \nat | Buffer\_buff! = Buffer\_buff ~] \end{zed} \begin{zed} Buffer\_OP\_size \defs [~ \Xi Buffer\_BufferState ; Buffer\_size! : 0 \upto maxbuff | Buffer\_size! = Buffer\_size ~] \end{zed} \begin{zed} Buffer\_BufferInit\_fOp \defs [~ \Xi Buffer\_BufferState | \lnot \pre Buffer\_BufferInit ~] \end{zed} \begin{zed} Buffer\_InputCmd\_fOp \defs [~ \Xi Buffer\_BufferState ; x? : \nat | \lnot \pre Buffer\_InputCmd ~] \end{zed} \begin{zed} Buffer\_OutputCmd\_fOp \defs [~ \Xi Buffer\_BufferState | \lnot \pre Buffer\_OutputCmd ~] \end{zed} \end{document} [DEBUG] ================= [End] Z in ZRM ======================== [DEBUG] ================= [Start] CSP ======================== [DEBUG] -- This CSP specification is translated from a Circus program by Circus2ZCSP translator. -- Minimum and maximum integers for model checking. Make sure they are set in advance. MININT = 0 MAXINT = 3 -- Maximum instances generated for iseq. Make sure it is set in advance. MAXINS = 3 -- include a set of libraries include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_basic.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_num.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_card.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_log.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_set.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_rel.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_fun.csp" include "/Users/ykf_2001/GoogleDrive/Study/Circus/trans_rules/cspm_library/lib_seq.csp" -- Axiomatic definition (Constant) -- They should be assigned manually to meet its type and predicate restriction -- and match the values assigned in Z as well -- The variables defined below should meet the predicate below -- maxbuff == 2 maxbuff = 2 -- type -- channel declarations channel div channel input,output : Nat channel Buffer_BufferInit-- channel Buffer_BufferInit_fOp -- channel Buffer_InputCmd: Nat-- !x channel Buffer_InputCmd_fOp: Nat -- !x channel Buffer_OutputCmd-- channel Buffer_OutputCmd_fOp -- channel Buffer_OP_size : {0 .. maxbuff} channel Buffer_OP_buff : fseq(Nat) -- hidden event HIDE_CSPB = {|Buffer_OP_size, Buffer_OP_buff, Buffer_BufferInit, Buffer_BufferInit_fOp, Buffer_InputCmd, Buffer_InputCmd_fOp, Buffer_OutputCmd, Buffer_OutputCmd_fOp|} -- processes for variable storing and retrieving -- processes -- Divergent Process DIV = div -> STOP Buffer = ( ( Buffer_BufferInit -> SKIP [] Buffer_BufferInit_fOp -> DIV ) ; let X = (Buffer_OP_buff?buff -> Buffer_OP_size?size -> ( ((size < maxbuff) & input?x -> ( Buffer_InputCmd!x -> SKIP [] Buffer_InputCmd_fOp!x -> DIV )) [] ((size > 0) & output.(head(buff)) -> ( Buffer_OutputCmd -> SKIP [] Buffer_OutputCmd_fOp -> DIV )) ) ; X) within X) MAIN = Buffer -- assertions assert MAIN :[ livelock free ] assert MAIN :[ deadlock free [F] ] assert MAIN :[ deadlock free [FD] ] [DEBUG] ================= [End] CSP ======================== [DEBUG] outputZCSPSpecToFile Done! Done!
Kangfeng (Randall) Ye (My Email: [email protected]). PhD Student in University of York. A member of the Circus team.