TAPAAL

Merge lp:~tapaal-contributor/tapaal/game-example-net into lp:tapaal

  1. game-example-net
  2. Merge into trunk
Proposed by Lena Ernstsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1082
Merged at revision: 1081
Proposed branch: lp:~tapaal-contributor/tapaal/game-example-net
Merge into: lp:tapaal
Diff against target: 141 lines (+42/-41)
1 file modified
src/resources/Example nets/game-harddisk.tapn (+42/-41)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/game-example-net
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Kenneth Yrke Jørgensen Approve
Review via email: mp+389150@code.launchpad.net

Commit message

Added an annotation and changed the constant

To post a comment you must log in.
Revision history for this message
Kenneth Yrke Jørgensen (yrke) :
review: Approve
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/resources/Example nets/game-harddisk.tapn'
2--- src/resources/Example nets/game-harddisk.tapn 2020-08-11 08:48:52 +0000
3+++ src/resources/Example nets/game-harddisk.tapn 2020-08-12 11:35:29 +0000
4@@ -4,8 +4,9 @@
5 <shared-place initialMarking="1" invariant="&lt; inf" name="R_2"/>
6 <shared-place initialMarking="0" invariant="&lt;= 10" name="Buffer"/>
7 <shared-place initialMarking="1" invariant="&lt; inf" name="R_1"/>
8- <constant name="D" value="3"/>
9+ <constant name="D" value="9"/>
10 <net active="true" id="harddisk_drive" type="P/T net">
11+ <labels border="true" height="51" positionX="632" positionY="347" width="148">If the global constant D is set to 8 or lower, then the "Never Fail" query will fail. </labels>
12 <place displayName="true" id="R_3" initialMarking="1" invariant="&lt; inf" name="R_3" nameOffsetX="-15" nameOffsetY="17" positionX="285" positionY="90"/>
13 <place displayName="true" id="W_3" initialMarking="0" invariant="&lt;= 4" name="W_3" nameOffsetX="44" nameOffsetY="-18" positionX="195" positionY="150"/>
14 <place displayName="true" id="track_3" initialMarking="0" invariant="&lt; inf" name="track_3" nameOffsetX="75" nameOffsetY="14" positionX="375" positionY="150"/>
15@@ -164,12 +165,12 @@
16 </arc>
17 <arc id="A33" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T13" target="Buffer" type="normal" weight="1">
18 <arcpath arcPointType="false" id="0" xCoord="204" yCoord="675"/>
19- <arcpath arcPointType="false" id="1" xCoord="139" yCoord="683"/>
20+ <arcpath arcPointType="false" id="1" xCoord="151" yCoord="695"/>
21 <arcpath arcPointType="false" id="2" xCoord="135" yCoord="464"/>
22 </arc>
23 <arc id="A34" inscription="[0,inf)" nameOffsetX="0" nameOffsetY="0" source="Buffer" target="T1" type="timed" weight="1">
24- <arcpath arcPointType="false" id="0" xCoord="135" yCoord="435"/>
25- <arcpath arcPointType="false" id="1" xCoord="140" yCoord="233"/>
26+ <arcpath arcPointType="false" id="0" xCoord="136" yCoord="435"/>
27+ <arcpath arcPointType="false" id="1" xCoord="152" yCoord="245"/>
28 <arcpath arcPointType="false" id="2" xCoord="204" yCoord="225"/>
29 </arc>
30 </net>
31@@ -186,73 +187,73 @@
32 <transition angle="0" displayName="false" id="T4" infiniteServer="false" name="T4" nameOffsetX="0" nameOffsetY="0" player="1" positionX="315" positionY="345" priority="0" urgent="false"/>
33 <transition angle="0" displayName="false" id="T5" infiniteServer="false" name="T5" nameOffsetX="0" nameOffsetY="0" player="1" positionX="405" positionY="345" priority="0" urgent="false"/>
34 <arc id="A0" inscription="[6,10]" nameOffsetX="0" nameOffsetY="6" source="Buffer" target="T0" type="timed" weight="1">
35- <arcpath arcPointType="false" id="0" xCoord="330" yCoord="105"/>
36- <arcpath arcPointType="false" id="1" xCoord="330" yCoord="165"/>
37+ <arcpath arcPointType="false" id="0" xCoord="342" yCoord="117"/>
38+ <arcpath arcPointType="false" id="1" xCoord="342" yCoord="177"/>
39 </arc>
40 <arc id="A1" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T0" target="R_2" type="normal" weight="1">
41- <arcpath arcPointType="false" id="0" xCoord="330" yCoord="195"/>
42- <arcpath arcPointType="false" id="1" xCoord="327" yCoord="236"/>
43- <arcpath arcPointType="false" id="2" xCoord="328" yCoord="255"/>
44+ <arcpath arcPointType="false" id="0" xCoord="342" yCoord="207"/>
45+ <arcpath arcPointType="false" id="1" xCoord="339" yCoord="248"/>
46+ <arcpath arcPointType="false" id="2" xCoord="340" yCoord="267"/>
47 </arc>
48 <arc id="A2" inscription="[D,D]" nameOffsetX="0" nameOffsetY="0" source="R_2" target="T4" type="timed" weight="1">
49- <arcpath arcPointType="false" id="0" xCoord="330" yCoord="285"/>
50- <arcpath arcPointType="false" id="1" xCoord="330" yCoord="345"/>
51+ <arcpath arcPointType="false" id="0" xCoord="342" yCoord="297"/>
52+ <arcpath arcPointType="false" id="1" xCoord="342" yCoord="357"/>
53 </arc>
54 <arc id="A3" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T4" target="Fail" type="normal" weight="1">
55- <arcpath arcPointType="false" id="0" xCoord="330" yCoord="375"/>
56- <arcpath arcPointType="false" id="1" xCoord="330" yCoord="435"/>
57+ <arcpath arcPointType="false" id="0" xCoord="342" yCoord="387"/>
58+ <arcpath arcPointType="false" id="1" xCoord="342" yCoord="447"/>
59 </arc>
60 <arc id="A6" inscription="[D,D]" nameOffsetX="0" nameOffsetY="0" source="R_3" target="T5" type="timed" weight="1">
61- <arcpath arcPointType="false" id="0" xCoord="420" yCoord="285"/>
62- <arcpath arcPointType="false" id="1" xCoord="420" yCoord="345"/>
63+ <arcpath arcPointType="false" id="0" xCoord="432" yCoord="297"/>
64+ <arcpath arcPointType="false" id="1" xCoord="432" yCoord="357"/>
65 </arc>
66 <arc id="A7" inscription="[D,D]" nameOffsetX="-3" nameOffsetY="5" source="R_1" target="T3" type="timed" weight="1">
67- <arcpath arcPointType="false" id="0" xCoord="240" yCoord="285"/>
68- <arcpath arcPointType="false" id="1" xCoord="240" yCoord="345"/>
69+ <arcpath arcPointType="false" id="0" xCoord="252" yCoord="297"/>
70+ <arcpath arcPointType="false" id="1" xCoord="252" yCoord="357"/>
71 </arc>
72 <arc id="A8" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T1" target="R_1" type="normal" weight="1">
73- <arcpath arcPointType="false" id="0" xCoord="240" yCoord="195"/>
74- <arcpath arcPointType="false" id="1" xCoord="238" yCoord="237"/>
75- <arcpath arcPointType="false" id="2" xCoord="239" yCoord="255"/>
76+ <arcpath arcPointType="false" id="0" xCoord="252" yCoord="207"/>
77+ <arcpath arcPointType="false" id="1" xCoord="250" yCoord="249"/>
78+ <arcpath arcPointType="false" id="2" xCoord="251" yCoord="267"/>
79 </arc>
80 <arc id="A9" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T2" target="R_3" type="normal" weight="1">
81- <arcpath arcPointType="false" id="0" xCoord="420" yCoord="195"/>
82- <arcpath arcPointType="false" id="1" xCoord="418" yCoord="238"/>
83- <arcpath arcPointType="false" id="2" xCoord="419" yCoord="255"/>
84+ <arcpath arcPointType="false" id="0" xCoord="432" yCoord="207"/>
85+ <arcpath arcPointType="false" id="1" xCoord="430" yCoord="250"/>
86+ <arcpath arcPointType="false" id="2" xCoord="431" yCoord="267"/>
87 </arc>
88 <arc id="I12" inscription="[0,inf)" nameOffsetX="0" nameOffsetY="0" source="R_1" target="T1" type="tapnInhibitor" weight="1">
89- <arcpath arcPointType="false" id="0" xCoord="249" yCoord="258"/>
90- <arcpath arcPointType="false" id="1" xCoord="267" yCoord="238"/>
91- <arcpath arcPointType="false" id="2" xCoord="240" yCoord="195"/>
92+ <arcpath arcPointType="false" id="0" xCoord="261" yCoord="270"/>
93+ <arcpath arcPointType="false" id="1" xCoord="279" yCoord="250"/>
94+ <arcpath arcPointType="false" id="2" xCoord="252" yCoord="207"/>
95 </arc>
96 <arc id="I13" inscription="[0,inf)" nameOffsetX="0" nameOffsetY="0" source="R_2" target="T0" type="tapnInhibitor" weight="1">
97- <arcpath arcPointType="false" id="0" xCoord="339" yCoord="258"/>
98- <arcpath arcPointType="false" id="1" xCoord="355" yCoord="237"/>
99- <arcpath arcPointType="false" id="2" xCoord="330" yCoord="195"/>
100+ <arcpath arcPointType="false" id="0" xCoord="351" yCoord="270"/>
101+ <arcpath arcPointType="false" id="1" xCoord="367" yCoord="249"/>
102+ <arcpath arcPointType="false" id="2" xCoord="342" yCoord="207"/>
103 </arc>
104 <arc id="I14" inscription="[0,inf)" nameOffsetX="0" nameOffsetY="0" source="R_3" target="T2" type="tapnInhibitor" weight="1">
105- <arcpath arcPointType="false" id="0" xCoord="429" yCoord="258"/>
106- <arcpath arcPointType="false" id="1" xCoord="447" yCoord="238"/>
107- <arcpath arcPointType="false" id="2" xCoord="420" yCoord="195"/>
108+ <arcpath arcPointType="false" id="0" xCoord="441" yCoord="270"/>
109+ <arcpath arcPointType="false" id="1" xCoord="459" yCoord="250"/>
110+ <arcpath arcPointType="false" id="2" xCoord="432" yCoord="207"/>
111 </arc>
112 <arc id="A14" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T3" target="Fail" type="normal" weight="1">
113- <arcpath arcPointType="false" id="0" xCoord="244" yCoord="360"/>
114- <arcpath arcPointType="false" id="1" xCoord="319" yCoord="439"/>
115+ <arcpath arcPointType="false" id="0" xCoord="256" yCoord="372"/>
116+ <arcpath arcPointType="false" id="1" xCoord="331" yCoord="451"/>
117 </arc>
118 <arc id="A15" inscription="1" nameOffsetX="0" nameOffsetY="0" source="T5" target="Fail" type="normal" weight="1">
119- <arcpath arcPointType="false" id="0" xCoord="414" yCoord="360"/>
120- <arcpath arcPointType="false" id="1" xCoord="340" yCoord="439"/>
121+ <arcpath arcPointType="false" id="0" xCoord="426" yCoord="372"/>
122+ <arcpath arcPointType="false" id="1" xCoord="352" yCoord="451"/>
123 </arc>
124 <arc id="A16" inscription="[6,10]" nameOffsetX="0" nameOffsetY="0" source="Buffer" target="T1" type="timed" weight="1">
125- <arcpath arcPointType="false" id="0" xCoord="319" yCoord="100"/>
126- <arcpath arcPointType="false" id="1" xCoord="244" yCoord="180"/>
127+ <arcpath arcPointType="false" id="0" xCoord="331" yCoord="112"/>
128+ <arcpath arcPointType="false" id="1" xCoord="256" yCoord="192"/>
129 </arc>
130 <arc id="A17" inscription="[6,10]" nameOffsetX="32" nameOffsetY="-6" source="Buffer" target="T2" type="timed" weight="1">
131- <arcpath arcPointType="false" id="0" xCoord="340" yCoord="100"/>
132- <arcpath arcPointType="false" id="1" xCoord="414" yCoord="180"/>
133+ <arcpath arcPointType="false" id="0" xCoord="352" yCoord="112"/>
134+ <arcpath arcPointType="false" id="1" xCoord="426" yCoord="192"/>
135 </arc>
136 </net>
137- <query active="true" approximationDenominator="2" capacity="4" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="null" gcd="false" hashTableSize="null" inclusionPlaces="*NONE*" name="Never Fail" overApproximation="true" pTrie="true" query="AG stream_requests.Fail &lt;= 0" reduction="true" reductionOption="VerifyTAPNdiscreteVerification" searchOption="DFS" symmetry="true" timeDarts="false" traceOption="NONE" useStubbornReduction="true"/>
138+ <query active="true" approximationDenominator="2" capacity="4" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="AUTOMATIC" gcd="false" hashTableSize="MB_16" inclusionPlaces="*NONE*" name="Never Fail" overApproximation="true" pTrie="true" query="AG stream_requests.Fail &lt;= 0" reduction="true" reductionOption="VerifyTAPNdiscreteVerification" searchOption="DFS" symmetry="true" timeDarts="false" traceOption="NONE" useStubbornReduction="true"/>
139 <k-bound bound="3"/>
140 <feature isGame="true" isTimed="true"/>
141 </pnml>

Subscribers

People subscribed via source and target branches