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
|
// 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 test_specifications.h
/// \brief Add your file description here.
#ifndef MCRL2_TEST_SPECIFICATIONS_H
#define MCRL2_TEST_SPECIFICATIONS_H
#include <string>
const std::string ABP_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";
#endif // MCRL2_TEST_SPECIFICATIONS_H
|
