1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://svn.win.tue.nl/trac/MCRL2/browser/trunk/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file lps_algorithm_test.cpp
/// \brief Add your file description here.
#include <iostream>
#include <iterator>
#include <boost/test/minimal.hpp>
#include "mcrl2/lps/detail/lps_algorithm.h"
#include "mcrl2/lps/specification.h"
#include "mcrl2/lps/linearise.h"
using namespace std;
using namespace mcrl2;
using namespace mcrl2::lps;
using namespace mcrl2::lps::detail;
std::string SPECIFICATION =
"% This file contains the alternating bit protocol, as described in W.J. \n"
"% Fokkink, J.F. Groote and M.A. Reniers, Modelling Reactive Systems. \n"
"% \n"
"% The only exception is that the domain D consists of two data elements to \n"
"% facilitate simulation. \n"
" \n"
"sort \n"
" D = struct d1 | d2; \n"
" Error = struct e; \n"
" \n"
"act \n"
" r1,s4: D; \n"
" s2,r2,c2: D # Bool; \n"
" s3,r3,c3: D # Bool; \n"
" s3,r3,c3: Error; \n"
" s5,r5,c5: Bool; \n"
" s6,r6,c6: Bool; \n"
" s6,r6,c6: Error; \n"
" i; \n"
" \n"
"proc \n"
" S(b:Bool) = sum d:D. r1(d).T(d,b); \n"
" T(d:D,b:Bool) = s2(d,b).(r6(b).S(!b)+(r6(!b)+r6(e)).T(d,b)); \n"
" \n"
" R(b:Bool) = sum d:D. r3(d,b).s4(d).s5(b).R(!b)+ \n"
" (sum d:D.r3(d,!b)+r3(e)).s5(!b).R(b); \n"
" \n"
" K = sum d:D,b:Bool. r2(d,b).(i.s3(d,b)+i.s3(e)).K; \n"
" \n"
" L = sum b:Bool. r5(b).(i.s6(b)+i.s6(e)).L; \n"
" \n"
"init \n"
" allow({r1,s4,c2,c3,c5,c6,i}, \n"
" comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6}, \n"
" S(true) || K || L || R(true) \n"
" ) \n"
" ); \n";
void test_remove_unused_summand_variables()
{
specification spec = linearise(SPECIFICATION);
lps::detail::lps_algorithm algorithm(spec);
algorithm.remove_unused_summand_variables();
}
int test_main(int argc, char** argv)
{
test_remove_unused_summand_variables();
return 0;
}
|
