LCOV - code coverage report
Current view: top level - lps/test - constelm_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 66 66 100.0 %
Date: 2020-07-04 00:44:36 Functions: 8 8 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file constelm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : //#define MCRL2_LPSCONSTELM_DEBUG
      13             : 
      14             : #define BOOST_TEST_MODULE constelm_test
      15             : #include "mcrl2/lps/constelm.h"
      16             : #include "mcrl2/lps/detail/specification_property_map.h"
      17             : #include "mcrl2/lps/detail/test_input.h"
      18             : #include "mcrl2/lps/linearise.h"
      19             : #include "mcrl2/lps/parse.h"
      20             : 
      21             : #include <boost/algorithm/string.hpp>
      22             : #include <boost/test/included/unit_test_framework.hpp>
      23             : 
      24             : using namespace mcrl2;
      25             : using namespace mcrl2::data;
      26             : using namespace mcrl2::lps;
      27             : 
      28           1 : std::string case_1 =
      29             :   "% Test Case 1 -- No Free Variables                                               \n"
      30             :   "%                                                                                \n"
      31             :   "% Process parameter i is substituted by 0 and removed from the list of process   \n"
      32             :   "% parameters.                                                                    \n"
      33             :   "                                                                                 \n"
      34             :   "act action :Nat;                                                                 \n"
      35             :   "                                                                                 \n"
      36             :   "proc P(i: Nat) = action(i). P(i);                                                \n"
      37             :   "                                                                                 \n"
      38             :   "init P(0);                                                                       \n"
      39             :   ;
      40           1 : const std::string expected_1 = "process_parameter_names =";
      41             : 
      42           1 : std::string case_2 =
      43             :   "% Test Case 2 -- No Free Variables                                               \n"
      44             :   "%                                                                                \n"
      45             :   "% Process parameter i will not be removed.                                       \n"
      46             :   "                                                                                 \n"
      47             :   "act action :Nat;                                                                 \n"
      48             :   "                                                                                 \n"
      49             :   "proc P(i: Nat) = action(i). P(i+1);                                              \n"
      50             :   "                                                                                 \n"
      51             :   "init P(0);                                                                       \n"
      52             :   ;
      53           1 : const std::string expected_2 = "process_parameter_names = i";
      54             : 
      55           1 : std::string case_3 =
      56             :   "% Test Case 3 -- No Free Variables                                               \n"
      57             :   "%                                                                                \n"
      58             :   "% Process parameter i will not be removed. Occurrences of process parameter j are\n"
      59             :   "% substituted by 5 and removed from the process parameter list.                  \n"
      60             :   "                                                                                 \n"
      61             :   "act action :Nat;                                                                 \n"
      62             :   "                                                                                 \n"
      63             :   "proc P(i, j: Nat) = action(j). P(i+1, j);                                        \n"
      64             :   "                                                                                 \n"
      65             :   "init P(0,5);                                                                     \n"
      66             :   ;
      67           1 : const std::string expected_3 = "process_parameter_names = i";
      68             : 
      69           1 : std::string case_4 =
      70             :   "% Test Case 4 -- No Free Variables                                               \n"
      71             :   "%                                                                                \n"
      72             :   "% Process parameter i will not be removed. Occurrences of process parameter j are\n"
      73             :   "% subtituted by 5 and removed from the process parameter list.                   \n"
      74             :   "%                                                                                \n"
      75             :   "% If --nocondition is used, occurrences of process parameters j are NOT          \n"
      76             :   "% substituted and removed. If --noreachable are summand                          \n"
      77             :   "% \"false -> action(j). P(i+1,j+1);\" will not be removed. If both options are   \n"
      78             :   "% used, the LPS remains the same.                                                \n"
      79             :   "                                                                                 \n"
      80             :   "act action :Nat;                                                                 \n"
      81             :   "                                                                                 \n"
      82             :   "proc P(i, j: Nat) = true  -> action(j). P(i+1,j)   +                             \n"
      83             :   "                    false -> action(j). P(i+1,j+1);                              \n"
      84             :   "                                                                                 \n"
      85             :   "init P(0,5);                                                                     \n"
      86             :   "                                                                                 \n"
      87             :   "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%                     \n"
      88             :   "%% NOTE:                                                  %%                     \n"
      89             :   "%% =====                                                  %%                     \n"
      90             :   "%%                                                        %%                     \n"
      91             :   "%% Use: mcrl22lps --no-cluster $DIR$/case4.mcrl2          %%                     \n"
      92             :   "%%                                                        %%                     \n"
      93             :   "%% Not using \"no-cluster\" will result in differt results. %%                   \n"
      94             :   "%%                                                        %%                     \n"
      95             :   "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%                     \n"
      96             :   ;
      97           1 : const std::string expected_4 = "process_parameter_names = i";
      98             : 
      99           1 : std::string case_5 =
     100             :   "% Test Case 5 -- No Free Variables                                               \n"
     101             :   "%                                                                                \n"
     102             :   "% Process parameter i will not be removed. Occurrences of process parameter j are\n"
     103             :   "% substituted by \"x\" and removed from the process parameter list.              \n"
     104             :   "%                                                                                \n"
     105             :   "% If \"--nosingleton\" is used, process parameter j are not substituted and      \n"
     106             :   "% not removed from the process parameter list.                                   \n"
     107             :   "                                                                                 \n"
     108             :   "sort Singleton = struct x;                                                       \n"
     109             :   "                                                                                 \n"
     110             :   "act  action :Nat;                                                                \n"
     111             :   "                                                                                 \n"
     112             :   "proc P(i : Nat, j : Singleton ) = true -> action(i). P(i+1,j);                   \n"
     113             :   "                                                                                 \n"
     114             :   "init P(0,x);                                                                     \n"
     115             :   ;
     116           1 : const std::string expected_5 = "process_parameter_names = i";
     117             : 
     118           1 : std::string case_6 =
     119             :   "% Test Case 6 -- No Free Variables                                               \n"
     120             :   "%                                                                                \n"
     121             :   "% Process parameter i is substituted by 0 and removed from the list of process   \n"
     122             :   "% parameters.                                                                    \n"
     123             :   "                                                                                 \n"
     124             :   "act action :Nat;                                                                 \n"
     125             :   "                                                                                 \n"
     126             :   "proc P(i: Nat) = action(i). Q(i);                                                \n"
     127             :   "     Q(i: Nat) = action(i). P(i);                                                \n"
     128             :   "                                                                                 \n"
     129             :   "init P(0);                                                                       \n"
     130             :   "                                                                                 \n"
     131             :   "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%                     \n"
     132             :   "%% NOTE:                                                  %%                     \n"
     133             :   "%% =====                                                  %%                     \n"
     134             :   "%%                                                        %%                     \n"
     135             :   "%% Usage of: mcrl22lps $DIR$/case6.mcrl2                  %%                     \n"
     136             :   "%% + indicates the second process parameter is constant   %%                     \n"
     137             :   "%% Usage of: mcrl22lps --no-cluster $DIR$/case6.mcrl2     %%                     \n"
     138             :   "%% + indicates the second process parameter is constant   %%                     \n"
     139             :   "%% In this case they are the same                         %%                     \n"
     140             :   "%%                                                        %%                     \n"
     141             :   "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%                     \n"
     142             :   ;
     143             : 
     144           1 : std::string case_6a =
     145             :   "%--- case 6 linearized ---%                                        \n"
     146             :   "act  action: Nat;                                                  \n"
     147             :   "                                                                   \n"
     148             :   "proc P(s3_P: Pos, i_P: Nat) =                                      \n"
     149             :   "       sum e_P: Bool.                                              \n"
     150             :   "         (if(e_P, true, true) && if(e_P, s3_P == 2, s3_P == 1)) -> \n"
     151             :   "         action(i_P) .                                             \n"
     152             :   "         P(if(e_P, 1, 2), i_P)                                     \n"
     153             :   "     + true ->                                                     \n"
     154             :   "         delta;                                                    \n"
     155             :   "                                                                   \n"
     156             :   "init P(1, 0);                                                      \n"
     157             :   ;
     158           1 : const std::string expected_6a = "process_parameter_names = s3_P";
     159             : 
     160           1 : std::string case_6b =
     161             :   "%--- case 6 linearized no-cluster ---%                             \n"
     162             :   "act  action: Nat;                                                  \n"
     163             :   "                                                                   \n"
     164             :   "proc P(s3_P: Pos, i_P: Nat) =                                      \n"
     165             :   "       (s3_P == 2) ->                                              \n"
     166             :   "         action(i_P) .                                             \n"
     167             :   "         P(1, i_P)                                                 \n"
     168             :   "     + (s3_P == 1) ->                                              \n"
     169             :   "         action(i_P) .                                             \n"
     170             :   "         P(2, i_P)                                                 \n"
     171             :   "     + true ->                                                     \n"
     172             :   "         delta;                                                    \n"
     173             :   "                                                                   \n"
     174             :   "init P(1, 0);                                                      \n"
     175             :   ;
     176           1 : const std::string expected_6b = "process_parameter_names = s3_P";
     177             : 
     178             : // % Test Case 7 -- Free Variables
     179             : // %
     180             : 
     181           1 : std::string case_7 =
     182             :   "glob  v: Nat ;                     \n"
     183             :   "                                   \n"
     184             :   "act a: Nat ;                       \n"
     185             :   "                                   \n"
     186             :   "proc P(i, j: Nat) =                \n"
     187             :   "       (i == j) -> a(i) . P(1, 1)  \n"
     188             :   "       ;                           \n"
     189             :   "                                   \n"
     190             :   "init P(i = 1, j = v) ;             \n"
     191             :   ;
     192           1 : const std::string expected_7 = "process_parameter_names = j";
     193             : 
     194             : // % Test Case 8 -- Free Variables
     195             : // %
     196             : // % No constant parameters are found
     197             : // %
     198             : // % lpsconstelm cannot detect (i==5)
     199             : //
     200             : // act action: Nat;
     201             : //
     202             : // proc X(i: Nat)   = (i <  5) -> action(i).X(i+1) +
     203             : //                    (i == 5) -> action(i).Y(i, i);
     204             : //      Y(i,j: Nat) = action(j).Y(i,j);
     205             : //
     206             : // init X(0);
     207             : //
     208             : // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     209             : // %% NOTE:                                                  %%
     210             : // %% =====                                                  %%
     211             : // %%                                                        %%
     212             : // %% Use: mcrl22lps --no-cluster $DIR$/case8.mcrl2          %%
     213             : // %%                                                        %%
     214             : // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     215             : //
     216             : // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     217             : // %%                                                        %%
     218             : // %% act  action: Nat;                                      %%
     219             : // %%                                                        %%
     220             : // %% var  freevar0: Nat;                                    %%
     221             : // %% proc P(s3: Pos, i,j: Nat) =                            %%
     222             : // %%       (s3 == 2) ->                                     %%
     223             : // %%         action(j) .                                    %%
     224             : // %%         P(s3 := 2)                                     %%
     225             : // %%     + (s3 == 1 && i < 5) ->                            %%
     226             : // %%         action(i) .                                    %%
     227             : // %%         P(s3 := 1, i := i + 1, j := freevar0)          %%
     228             : // %%     + (s3 == 1 && i == 5) ->                           %%
     229             : // %%         action(i) .                                    %%
     230             : // %%         P(s3 := 2, j := i);                            %%
     231             : // %%                                                        %%
     232             : // %% var  freevar: Nat;                                     %%
     233             : // %% init P(s3 := 1, i := 0, j := freevar);                 %%
     234             : // %%                                                        %%
     235             : // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     236           1 : std::string case_8 =
     237             :   "act  action: Nat;                 \n"
     238             :   "                                  \n"
     239             :   "var  dc1: Nat;                    \n"
     240             :   "proc P(s3_X: Pos, i_X,j_X: Nat) = \n"
     241             :   "       (s3_X == 2) ->             \n"
     242             :   "         action(j_X) .            \n"
     243             :   "         P(2, i_X, j_X)           \n"
     244             :   "     + (s3_X == 1 && i_X == 5) -> \n"
     245             :   "         action(i_X) .            \n"
     246             :   "         P(2, i_X, i_X)           \n"
     247             :   "     + (s3_X == 1 && i_X < 5) ->  \n"
     248             :   "         action(i_X) .            \n"
     249             :   "         P(1, i_X + 1, dc1);      \n"
     250             :   "                                  \n"
     251             :   "var  dc: Nat;                     \n"
     252             :   "init P(1, 0, dc);                 \n"
     253             :   ;
     254           1 : const std::string expected_8 = "process_parameter_names = ";
     255             : 
     256             : // examples/games/domineering.mcrl2
     257           1 : std::string case_9 =
     258             :   "sort Position = struct F | E;\n"
     259             :   "Row = List(Position);\n"
     260             :   "Board = List(List(Position));\n"
     261             :   "\n"
     262             :   "map  Put: Position # Pos # List(Position) -> List(Position);\n"
     263             :   "Put: Position # Pos # Pos # List(List(Position)) -> List(List(Position));\n"
     264             :   "At: Pos # Pos # List(List(Position)) -> Position;\n"
     265             :   "At: Pos # List(Position) -> Position;\n"
     266             :   "N,M: Pos;\n"
     267             :   "NoHorizontalSpot,NoVerticalSpot: Pos # Pos # List(List(Position)) -> Bool;\n"
     268             :   "\n"
     269             :   "var  b: List(List(Position));\n"
     270             :   "r: List(Position);\n"
     271             :   "p,p': Position;\n"
     272             :   "x,y: Pos;\n"
     273             :   "eqn  N  =  5;\n"
     274             :   "M  =  5;\n"
     275             :   "At(x, y, [])  =  E;\n"
     276             :   "y == 1  ->  At(x, y, r |> b)  =  At(x, r);\n"
     277             :   "y > 1  ->  At(x, y, r |> b)  =  At(x, Int2Pos(y - 1), b);\n"
     278             :   "At(y, [])  =  E;\n"
     279             :   "x == 1  ->  At(x, p |> r)  =  p;\n"
     280             :   "x > 1  ->  At(x, p |> r)  =  At(Int2Pos(x - 1), r);\n"
     281             :   "y == 1  ->  Put(p, x, y, r |> b)  =  Put(p, x, r) |> b;\n"
     282             :   "y > 1  ->  Put(p, x, y, r |> b)  =  r |> Put(p, x, Int2Pos(y - 1), b);\n"
     283             :   "x == 1  ->  Put(p, x, p' |> r)  =  p |> r;\n"
     284             :   "x > 1  ->  Put(p, x, p' |> r)  =  p' |> Put(p, Int2Pos(x - 1), r);\n"
     285             :   "y == M  ->  NoVerticalSpot(x, y,b)  =  true;\n"
     286             :   "x < N && y < M  ->  NoVerticalSpot(x, y, b)  =  (At(x, y, b) == F || At(x, y + 1, b) == F) && NoVerticalSpot(x + 1, y, b);\n"
     287             :   "x == N && y < M  ->  NoVerticalSpot(x, y, b)  =  (At(x, y, b) == F || At(x, y + 1, b) == F) && NoVerticalSpot(1, y + 1, b);\n"
     288             :   "x == N  ->  NoHorizontalSpot(x, y,b)  =  true;\n"
     289             :   "x < N && y < M  ->  NoHorizontalSpot(x, y, b)  =  (At(x, y, b) == F || At(x + 1, y, b) == F) && NoHorizontalSpot(x, y + 1, b);\n"
     290             :   "x < N && y == M  ->  NoHorizontalSpot(x, y, b)  =  (At(x, y, b) == F || At(x + 1, y, b) == F) && NoHorizontalSpot(x + 1, 1, b);\n"
     291             :   "\n"
     292             :   "act  Player1,Player2: Pos # Pos # Pos # Pos;\n"
     293             :   "Player1Wins,Player2Wins;\n"
     294             :   "\n"
     295             :   "proc P(b: List(List(struct F | E)), c: Bool) =\n"
     296             :   "(c && (At(1,1,b) == F || At(1,2,b) == F) && (At(2,1,b) == F || At(2,2,b) == F) && (At(3,1,b) == F || At(3,2,b) == F) && (At(4,1,b) == F || At(4,2,b) == F) && (At(5,1,b) == F || At(5,2,b) == F) && (At(1,2,b) == F || At(1,3,b) == F) && (At(2,2,b) == F || At(2,3,b) == F) && (At(3,2,b) == F || At(3,3,b) == F) && (At(4,2,b) == F || At(4,3,b) == F) && (At(5,2,b) == F || At(5,3,b) == F) && (At(1,3,b) == F || At(1,4,b) == F) && (At(2,3,b) == F || At(2,4,b) == F) && (At(3,3,b) == F || At(3,4,b) == F) && (At(4,3,b) == F || At(4,4,b) == F) && (At(5,3,b) == F || At(5,4,b) == F) && (At(1,4,b) == F || At(1,5,b) == F) && (At(2,4,b) == F || At(2,5,b) == F) && (At(3,4,b) == F || At(3,5,b) == F) && (At(4,4,b) == F || At(4,5,b) == F) && At(5,4,b) == F || At(5,5,b) == F) ->\n"
     297             :   "Player2Wins .\n"
     298             :   "P(b, c)\n"
     299             :   "+ sum x1,y1: Pos.\n"
     300             :   "(!c && x1 < 5 && y1 <= 5 && At(x1, y1, b) == E && At(succ(x1), y1, b) == E) ->\n"
     301             :   "Player2(x1, y1, x1 + 1, y1) .\n"
     302             :   "P(Put(F, succ(x1), y1, Put(F, x1, y1, b)), true)\n"
     303             :   "+ (!c && (At(1,1,b) == F || At(2,1,b) == F) && (At(1,2,b) == F || At(2,2,b) == F) && (At(1,3,b) == F || At(2,3,b) == F) && (At(1,4,b) == F || At(2,4,b) == F) && (At(1,5,b) == F || At(2,5,b) == F) && (At(2,1,b) == F || At(3,1,b) == F) && (At(2,2,b) == F || At(3,2,b) == F) && (At(2,3,b) == F || At(3,3,b) == F) && (At(2,4,b) == F || At(3,4,b) == F) && (At(2,5,b) == F || At(3,5,b) == F) && (At(3,1,b) == F || At(4,1,b) == F) && (At(3,2,b) == F || At(4,2,b) == F) && (At(3,3,b) == F || At(4,3,b) == F) && (At(3,4,b) == F || At(4,4,b) == F) && (At(3,5,b) == F || At(4,5,b) == F) && (At(4,1,b) == F || At(5,1,b) == F) && (At(4,2,b) == F || At(5,2,b) == F) && (At(4,3,b) == F || At(5,3,b) == F) && (At(4,4,b) == F || At(5,4,b) == F) && At(4,5,b) == F || At(5,5,b) == F) ->\n"
     304             :   "Player1Wins .\n"
     305             :   "P(b, c)\n"
     306             :   "+ sum x,y: Pos.\n"
     307             :   "(c && x <= 5 && y < 5 && At(x, y, b) == E && At(x, succ(y), b) == E) ->\n"
     308             :   "Player1(x, y, x, y + 1) .\n"
     309             :   "P(Put(F, x, succ(y), Put(F, x, y, b)), false)\n"
     310             :   "+ true ->\n"
     311             :   "delta;\n"
     312             :   "\n"
     313             :   "init P((E |> E |> E |> E |> E |> []) |> (E |> E |> E |> E |> E |> []) |> (E |> E |> E |> E |> E |> []) |> (E |> E |> E |> E |> E |> []) |> (E |> E |> E |> E |> E |> []) |> [], true);\n"
     314             :   ;
     315           1 : const std::string expected_9 = "process_parameter_names = b, c";
     316             : 
     317             : // Test case provided by Jan Friso Groote (2-9-2009). It is based on the process
     318             : //
     319             : // act  a:Bool;
     320             : // proc X(p:List(Bool))=sum b:Bool.a(head(p)).X(b|>tail(p)); init X([true]);
     321             : //
     322             : // The list has always length one. After application of lpsconstelm, only one of the
     323             : // three parameters should remain.
     324             : //
     325             : // Before linearization:
     326             : //
     327             : // sort S11;
     328             : //
     329             : // cons c_1,c_2: S11;
     330             : //
     331             : // map  C_S11_1: S11 # List(Bool) # List(Bool) -> List(Bool);
     332             : //      pi_S11_2: List(Bool) -> List(Bool);
     333             : //      pi_S11_1: List(Bool) -> Bool;
     334             : //      Det_S11_1: List(Bool) -> S11;
     335             : //
     336             : // var  y3,y4,d3: List(Bool);
     337             : //      y2: S11;
     338             : //      d2: Bool;
     339             : // eqn  C_S11_1(c_1, y3, y4)  =  y3;
     340             : //      C_S11_1(c_2, y3, y4)  =  y4;
     341             : //      C_S11_1(y2, y4, y4)  =  y4;
     342             : //      Det_S11_1([])  =  c_1;
     343             : //      Det_S11_1(d2 |> d3)  =  c_2;
     344             : //      pi_S11_1(d2 |> d3)  =  d2;
     345             : //      pi_S11_2(d2 |> d3)  =  d3;
     346             : //
     347             : // act  a: Bool;
     348             : //
     349             : // proc P(S1_pp1: S11, S1_pp2: Bool, S1_pp3: List(Bool)) =
     350             : //        sum b_X: Bool.
     351             : //          a(head(C_S11_1(S1_pp1, [], S1_pp2 |> S1_pp3))) .
     352             : //          P(S1_pp1 = Det_S11_1(b_X |> tail(C_S11_1(S1_pp1, [], S1_pp2 |> S1_pp3))), S1_pp2 = pi_S11_1(b_X |> tail(C_S11_1(S1_pp1, [], S1_pp2 |> S1_pp3))), S1_pp3 = pi_S11_2(b_X |> tail(C_S11_1(S1_pp1, [], S1_pp2 |> S1_pp3))))
     353             : //      + true ->
     354             : //          delta;
     355             : //
     356             : // init P(Det_S11_1(true |> []), pi_S11_1(true |> []), pi_S11_2(true |> []));
     357             : //
     358           1 : std::string case_10 =
     359             :   "sort S11;                                                                                                    \n"
     360             :   "                                                                                                             \n"
     361             :   "cons c_1,c_2: S11;                                                                                           \n"
     362             :   "                                                                                                             \n"
     363             :   "map  C_S11_1: S11 # List(Bool) # List(Bool) -> List(Bool);                                                   \n"
     364             :   "     pi_S11_2: List(Bool) -> List(Bool);                                                                     \n"
     365             :   "     pi_S11_1: List(Bool) -> Bool;                                                                           \n"
     366             :   "     Det_S11_1: List(Bool) -> S11;                                                                           \n"
     367             :   "                                                                                                             \n"
     368             :   "var  y3,y4,d3: List(Bool);                                                                                   \n"
     369             :   "     y2: S11;                                                                                                \n"
     370             :   "     d2: Bool;                                                                                               \n"
     371             :   "eqn  C_S11_1(c_1, y3, y4)  =  y3;                                                                            \n"
     372             :   "     C_S11_1(c_2, y3, y4)  =  y4;                                                                            \n"
     373             :   "     C_S11_1(y2, y4, y4)  =  y4;                                                                             \n"
     374             :   "     Det_S11_1([])  =  c_1;                                                                                  \n"
     375             :   "     Det_S11_1(d2 |> d3)  =  c_2;                                                                            \n"
     376             :   "     pi_S11_1(d2 |> d3)  =  d2;                                                                              \n"
     377             :   "     pi_S11_2(d2 |> d3)  =  d3;                                                                              \n"
     378             :   "                                                                                                             \n"
     379             :   "act  a: Bool;                                                                                                \n"
     380             :   "                                                                                                             \n"
     381             :   "proc P(S1_pp1_P: S11, S1_pp2_P: Bool, S1_pp3_P: List(Bool)) =                                                \n"
     382             :   "       sum b_X_P: Bool.                                                                                      \n"
     383             :   "         true ->                                                                                             \n"
     384             :   "         a(head(C_S11_1(S1_pp1_P, [], S1_pp2_P |> S1_pp3_P))) .                                              \n"
     385             :   "         P(S1_pp1_P = c_2, S1_pp2_P = b_X_P, S1_pp3_P = tail(C_S11_1(S1_pp1_P, [], S1_pp2_P |> S1_pp3_P)));  \n"
     386             :   "                                                                                                             \n"
     387             :   "init P(Det_S11_1(true |> []), pi_S11_1(true |> []), pi_S11_2(true |> []));                                   \n"
     388             :   ;
     389             : 
     390           1 : const std::string expected_10 = "process_parameter_count = 1";
     391             : 
     392          10 : void test_constelm(const std::string& message, const std::string& spec_text, const std::string& expected_result)
     393             : {
     394          20 :   specification spec = parse_linear_process_specification(spec_text);
     395          20 :   data::rewriter R(spec.data());
     396          10 :   bool instantiate_free_variables = false;
     397          10 :   constelm(spec, R, instantiate_free_variables);
     398          20 :   lps::detail::specification_property_map<> info(spec);
     399          10 :   BOOST_CHECK(data::detail::compare_property_maps(message, info, expected_result));
     400          10 : }
     401             : 
     402           1 : void test_constelm()
     403             : {
     404           1 :   test_constelm("case_1" , case_1,  expected_1);
     405           1 :   test_constelm("case_2" , case_2,  expected_2);
     406           1 :   test_constelm("case_3" , case_3,  expected_3);
     407           1 :   test_constelm("case_4" , case_4,  expected_4);
     408           1 :   test_constelm("case_5" , case_5,  expected_5);
     409           1 :   test_constelm("case_6a", case_6a, expected_6a);
     410           1 :   test_constelm("case_6b", case_6b, expected_6b);
     411           1 :   test_constelm("case_7" , case_7,  expected_7);
     412             :   // test_constelm("case_8" , case_8,  expected_8);
     413           1 :   test_constelm("case_9" , case_9,  expected_9);
     414           1 :   test_constelm("case_10" , case_10,  expected_10);
     415           1 : }
     416             : 
     417           1 : void test_abp()
     418             : {
     419           2 :   stochastic_specification spec = linearise(lps::detail::ABP_SPECIFICATION());
     420           2 :   data::rewriter R(spec.data());
     421           1 :   bool instantiate_free_variables = false;
     422           1 :   constelm(spec, R, instantiate_free_variables);
     423           1 :   BOOST_CHECK(check_well_typedness(spec));
     424           1 : }
     425             : 
     426           1 : void test_stochastic_specification()
     427             : {
     428             :   std::string text =
     429             :     "act action :Nat;                                     \n"
     430             :     "                                                     \n"
     431             :     "proc P(i, j: Nat) = true  -> action(j). P(i+1,j)   + \n"
     432             :     "                    false -> action(j). P(i+1,j+1);  \n"
     433             :     "                                                     \n"
     434             :     "init P(0,5);                                         \n"
     435           2 :     "                                                     \n"
     436             :     ;
     437           2 :   std::string expected_result = "process_parameter_names = i";
     438           2 :   stochastic_specification spec;
     439           1 :   parse_lps(text, spec);
     440           2 :   data::rewriter R(spec.data());
     441           1 :   bool instantiate_free_variables = false;
     442           1 :   constelm(spec, R, instantiate_free_variables);
     443           2 :   lps::detail::specification_property_map<stochastic_specification> info(spec);
     444           1 :   BOOST_CHECK(data::detail::compare_property_maps("test_stochastic_specification", info, expected_result));
     445           1 : }
     446             : 
     447           3 : BOOST_AUTO_TEST_CASE(test_main)
     448             : {
     449           1 :   test_constelm();
     450           1 :   test_abp();
     451           1 :   test_stochastic_specification();
     452           4 : }
     453             : 

Generated by: LCOV version 1.13