examples/ReadWriteConflict/ReadWriteTestPurposes.txs at main · TorXakis/examples · GitHub

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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
{-
TorXakis - Model Based Testing
Copyright (c) 2015-2017 TNO and Radboud University
See LICENSE at root directory of this repository.
-}

TYPEDEF MemoryAccess ::= MemoryAccess { identity :: String; value :: Int }
ENDDEF

PROCDEF cell [ Read, Write :: MemoryAccess ] ( value :: Int ) ::=
        Read ? ma [[ value (ma) == value]] >-> cell [Read, Write ] (value)
    ##
        Write ? ma >->  cell [Read, Write] (value (ma))
ENDDEF


PROCDEF plus [ Read, Write :: MemoryAccess ] ( myName :: String; n :: Int ) EXIT ::=
    Read ? ma [[ identity (ma) == myName]] >-> Write ! MemoryAccess (myName, value (ma)+n) >-> EXIT
ENDDEF


PROCDEF readWrite [ Read, Write :: MemoryAccess ] ( ) ::=
             plus [ Read, Write ]("p1",1)
         |||
             plus [ Read, Write ]("p2",2)
         |||
             plus [ Read, Write ]("p3",4)
     >>>
              Read ? ma [[ identity (ma) == "Final"]]
         >->  Write ! MemoryAccess("Reset",0)
         >->  readWrite [ Read, Write ] ( )
ENDDEF


PROCDEF system [ Read, Write :: MemoryAccess ] ( ) ::=
        cell [ Read, Write ] ( 0 )
    |[ Read, Write ]|
        readWrite [ Read, Write ] ( )
ENDDEF

CHANDEF Channels ::=
    Read, Write, Dummy :: MemoryAccess
ENDDEF

MODELDEF Model ::=
    CHAN IN Dummy
    CHAN OUT  Read, Write

	BEHAVIOUR
              system [ Read, Write ] ( )
ENDDEF


-- -------------------------------------------------------- --
-- Test Purpose to prove that all outcomes [1..7] are obtained
-----------------------------------------------------------------

PROCDEF output [Read, Write :: MemoryAccess](n :: Int) HIT ::=
        Read ! MemoryAccess ("Final",n) >-> HIT
    ##
        Read ? ma [[ (identity(ma) <> "Final") \/ (value(ma) <> n)]] >-> output [Read, Write](n)
    ##
        Write ? ma >-> output [Read, Write](n)
ENDDEF

PURPDEF HitAll ::=
    CHAN IN   Dummy
    CHAN OUT  Read, Write

    GOAL Hit1 ::= output [Read, Write] (1)
    GOAL Hit2 ::= output [Read, Write] (2)
    GOAL Hit3 ::= output [Read, Write] (3)
    GOAL Hit4 ::= output [Read, Write] (4)
    GOAL Hit5 ::= output [Read, Write] (5)
    GOAL Hit6 ::= output [Read, Write] (6)
    GOAL Hit7 ::= output [Read, Write] (7)
ENDDEF

CNECTDEF  Sut ::=
    CLIENTSOCK

    CHAN OUT Dummy                   HOST "localhost"  PORT 7776
    ENCODE   Dummy ? s               -> ! toString(s)
    CHAN IN  Read                    HOST "localhost"  PORT 7777
    DECODE   Read ! fromString(s)    <- ? s
    CHAN IN  Write                   HOST "localhost"  PORT 7778
    DECODE   Write ! fromString(s)   <- ? s
ENDDEF

CNECTDEF  Sim ::=
    SERVERSOCK

    CHAN IN   Dummy                   HOST "localhost"  PORT 7776
    DECODE    Dummy ! fromString(s)   <- ? s
    CHAN OUT  Read                    HOST "localhost"  PORT 7777
    ENCODE    Read ? b                ->  ! toString(b)
    CHAN OUT  Write                   HOST "localhost"  PORT 7778
    ENCODE    Write ? b               ->  ! toString(b)
ENDDEF