Analysis of a concurrent calculation

--- This page is still under construction. ---


1. Process Definition

We show some results of the analysis of a concurrent process CAL(N) defined by Fig.1.

   CAL(N) = (SQREM(N) [|{|rem,end2|}|] SUM(0)) \ {|rem,end2|}
 SQREM(n) = (SQ(n) [|{|sq,end1|}|] REM) \ {|sq,end1|}
    SQ(n) = ((n>0) & in?x1 -> sq!(x1*x1) -> SQ(n-1)) [] ((n==0) & end1!0 -> STOP)
      REM = sq?x2 -> rem!(x2%10) -> REM [] end1?z1 -> end2!z1 -> STOP
   SUM(y) = rem?x3 -> prt!x3 -> SUM(y+x3) [] end2?z2 -> prts!y -> STOP

Fig.1. CSPM script of CAL(N)




Fig.2. The structure of CAL(N)


2. Process Analysis by CONPASU

The symbolic transition graphs generated by CONPASU from CAL(N) are shown in Figs.3 and 4. Graphviz is used for drawing these graphs.



Fig.3. The symbolic transition graph of CAL(N) generated by CONPASU from Fig.1   (Click the graph to magnify it)


Fig.4. The symbolic transition graph after the state-reduction from Fig.3   (Click the graph to magnify it)


CONPASU can extract abstract behavior from concurrent processes. For example, Fig.5 shows the transition graph of ACAL(n) obtained by focusing the channels in and prts, thus by hiding the channel prt (ACAL(N) = CAL(N)\{|prt|}.


Fig.5. The symbolic transition graph of ACAL(n) generated by CONPASU from Fig.1 (Click the graph to magnify it)

3. Related work

The standard transition graphs generated by PAT, LTSA, and mCRL2 which are well-known model checkers, are shown in Figs.6, 7 and 8.



Fig.6. The transition graph of CAL(3) generated by PAT, where the input values are 0 or 1  (Click the graph to magnify it)


Fig.7. The minimized transition graph of CAL(3) generated by LTSA, where the input values are 0 or 1 (Click the graph to magnify it)


Fig.8. The minimized transition graph of CAL(3) generated by mCRL2, where the input values are in {0,...,23}.

4. Collaboration with model checkers

CONPASU can be used as a pre-process of model checkers for reducing the size of states. For example, Fig.9 shows the numbers of states used for checking failures-equivalence between CAL and SPEC based on ground operational semantics with symbolic operational semantics. CONPASU allows us to check the equivalence between CAL and SPEC by checking SPEC and  SEQ generated by CONPASU. It means that we do not have to generate the labeled transition system, which has 10,944 states from CAL. (note: FDR has various good methods of compression based on ground semantics)




Fig.9. The numbers of states used for checking the branching equivalence between CAL and SPEC