verifypn

Merge lp:~jespoke/verifypn/relevant-inhib-fix into lp:verifypn

  1. relevant-inhib-fix
  2. Merge into new-trunk
Proposed by Jesper Adriaan Van Diepen
Status: Merged
Merged at revision: 255
Proposed branch: lp:~jespoke/verifypn/relevant-inhib-fix
Merge into: lp:verifypn
Diff against target: 290 lines (+252/-5)
3 files modified
src/PetriEngine/Reducer.cpp (+10/-5)
test_models/inhibitor-relevance-test001/model.pnml (+206/-0)
test_models/inhibitor-relevance-test001/query.xml (+36/-0)
To merge this branch: bzr merge lp:~jespoke/verifypn/relevant-inhib-fix
Reviewer Review Type Date Requested Status
VerifyPN Maintainers Pending
Review via email: mp+410045@code.launchpad.net

Commit message

In Reducer.cpp, function 'relevant', block for dealing with inhibitor arcs.

Removed the condition in the loop iterating it2 that would break the loop when arc it2 is an inhibitor. This is to ensure the loop breaks on exactly the arc from place, which we know to exist at that point.
Inserted a condition to continue if that found arc is an inhibitor, as that means it cannot consume tokens.
Inserted a condition to continue if a decreasing loop is unable to lower the marking of place far enough to disable the inhibitor under evaluation.
On the same line, flipped the <= to >= in the existing condition, as the continue should happen on non-decreasing loops, not non-increasing ones.

Also included a test model which is affected by this change.

Description of the change

In Reducer.cpp, function 'relevant', block for dealing with inhibitor arcs.

Fix for a problem that can cause the the function 'relevant' to produce different conclusions on what parts of the model are relevant depending on the internal order of places, and on the relative weights of an inhibitor arc and a regular arc between the same place and transition as if they could form a decreasing loop.

Added a condition to not consider a decreasing loop relevant to an inhibitor arc if it cannot lower the marking on their shared place below the inhibitor's weight.

Included a test where two equivalent queries on identical models result in different reduced nets without the fix.

To post a comment you must log in.
Revision history for this message
Peter Gjøl Jensen (peter-gjoel) :
Revision history for this message
Jesper Adriaan Van Diepen (jespoke) :

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/PetriEngine/Reducer.cpp'
2--- src/PetriEngine/Reducer.cpp 2021-07-07 13:19:23 +0000
3+++ src/PetriEngine/Reducer.cpp 2021-10-12 10:06:40 +0000
4@@ -1535,23 +1535,28 @@
5 if (arc.inhib) {
6 for (auto pt : place.consumers) {
7 if (!tseen[pt]) {
8+ // Summary of block: 'pt' is seen unless it:
9+ // - Is inhibited by 'place'
10+ // - Forms a decreasing loop on 'place' that cannot lower the marking of 'place' below the weight of 'arc'
11+ // - Forms a non-decreasing loop on 'place'
12 Transition &trans = parent->_transitions[pt];
13 auto it = trans.post.begin();
14 for (; it != trans.post.end(); ++it)
15 if (it->place >= arc.place) break;
16+
17 if (it != trans.post.end() && it->place == arc.place) {
18 auto it2 = trans.pre.begin();
19+ // Find the arc from place to trans we know to exist because that is how we found trans in the first place
20 for (; it2 != trans.pre.end(); ++it2)
21- if (it2->place >= arc.place || it2->inhib) break;
22- if (it->weight <= it2->weight) continue;
23+ if (it2->place >= arc.place) break;
24+ // No need for a || it2->place != arc.place condition because we know the loop will always break on it2->place == arc.place
25+ if (it2->inhib || it->weight >= arc.weight || it->weight >= it2->weight) continue;
26 }
27- tseen[pt] = true;
28- wtrans.push_back(pt);
29- }
30 }
31 } else {
32 for (auto pt : place.producers) {
33 if (!tseen[pt]) {
34+ // Summary of block: pt is seen unless it forms a non-increasing loop on place
35 Transition &trans = parent->_transitions[pt];
36 auto it = trans.pre.begin();
37 for (; it != trans.pre.end(); ++it)
38
39=== added directory 'test_models/inhibitor-relevance-test001'
40=== added file 'test_models/inhibitor-relevance-test001/model.pnml'
41--- test_models/inhibitor-relevance-test001/model.pnml 1970-01-01 00:00:00 +0000
42+++ test_models/inhibitor-relevance-test001/model.pnml 2021-10-12 10:06:40 +0000
43@@ -0,0 +1,206 @@
44+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
45+<pnml xmlns="http://www.pnml.org/version-2009/grammar/pnml">
46+ <net id="ComposedModel" type="http://www.pnml.org/version-2009/grammar/ptnet">
47+ <page id="page0">
48+ <place id="P0">
49+ <graphics>
50+ <position x="465" y="300"/>
51+ </graphics>
52+ <name>
53+ <graphics>
54+ <offset x="9" y="-1"/>
55+ </graphics>
56+ <text>P0</text>
57+ </name>
58+ <initialMarking>
59+ <text>1</text>
60+ </initialMarking>
61+ </place>
62+ <place id="P1">
63+ <graphics>
64+ <position x="315" y="300"/>
65+ </graphics>
66+ <name>
67+ <graphics>
68+ <offset x="13" y="-6"/>
69+ </graphics>
70+ <text>P1</text>
71+ </name>
72+ <initialMarking>
73+ <text>2</text>
74+ </initialMarking>
75+ </place>
76+ <place id="P2">
77+ <graphics>
78+ <position x="195" y="330"/>
79+ </graphics>
80+ <name>
81+ <graphics>
82+ <offset x="0" y="0"/>
83+ </graphics>
84+ <text>P2</text>
85+ </name>
86+ <initialMarking>
87+ <text>0</text>
88+ </initialMarking>
89+ </place>
90+ <place id="P3">
91+ <graphics>
92+ <position x="195" y="240"/>
93+ </graphics>
94+ <name>
95+ <graphics>
96+ <offset x="0" y="0"/>
97+ </graphics>
98+ <text>P3</text>
99+ </name>
100+ <initialMarking>
101+ <text>1</text>
102+ </initialMarking>
103+ </place>
104+ <place id="P4">
105+ <graphics>
106+ <position x="345" y="540"/>
107+ </graphics>
108+ <name>
109+ <graphics>
110+ <offset x="0" y="-2"/>
111+ </graphics>
112+ <text>P4</text>
113+ </name>
114+ <initialMarking>
115+ <text>2</text>
116+ </initialMarking>
117+ </place>
118+ <place id="P5">
119+ <graphics>
120+ <position x="495" y="540"/>
121+ </graphics>
122+ <name>
123+ <graphics>
124+ <offset x="11" y="-1"/>
125+ </graphics>
126+ <text>P5</text>
127+ </name>
128+ <initialMarking>
129+ <text>1</text>
130+ </initialMarking>
131+ </place>
132+ <place id="P6">
133+ <graphics>
134+ <position x="210" y="510"/>
135+ </graphics>
136+ <name>
137+ <graphics>
138+ <offset x="0" y="0"/>
139+ </graphics>
140+ <text>P6</text>
141+ </name>
142+ <initialMarking>
143+ <text>1</text>
144+ </initialMarking>
145+ </place>
146+ <place id="P7">
147+ <graphics>
148+ <position x="210" y="570"/>
149+ </graphics>
150+ <name>
151+ <graphics>
152+ <offset x="0" y="0"/>
153+ </graphics>
154+ <text>P7</text>
155+ </name>
156+ <initialMarking>
157+ <text>0</text>
158+ </initialMarking>
159+ </place>
160+ <transition id="T0">
161+ <name>
162+ <graphics>
163+ <offset x="22" y="-14"/>
164+ </graphics>
165+ <text>T0</text>
166+ </name>
167+ <graphics>
168+ <position x="405" y="300"/>
169+ </graphics>
170+ </transition>
171+ <transition id="T1">
172+ <name>
173+ <graphics>
174+ <offset x="14" y="-10"/>
175+ </graphics>
176+ <text>T1</text>
177+ </name>
178+ <graphics>
179+ <position x="255" y="300"/>
180+ </graphics>
181+ </transition>
182+ <transition id="T2">
183+ <name>
184+ <graphics>
185+ <offset x="27" y="-15"/>
186+ </graphics>
187+ <text>T2</text>
188+ </name>
189+ <graphics>
190+ <position x="435" y="540"/>
191+ </graphics>
192+ </transition>
193+ <transition id="T3">
194+ <name>
195+ <graphics>
196+ <offset x="27" y="-15"/>
197+ </graphics>
198+ <text>T3</text>
199+ </name>
200+ <graphics>
201+ <position x="270" y="540"/>
202+ </graphics>
203+ </transition>
204+ <arc id="P3_to_T1" source="P3" target="T1" type="normal"/>
205+ <arc id="P1_to_T0" source="P1" target="T0" type="normal">
206+ <inscription>
207+ <text>2</text>
208+ </inscription>
209+ <graphics>
210+ <position x="377" y="349"/>
211+ </graphics>
212+ </arc>
213+ <arc id="P6_to_T3" source="P6" target="T3" type="normal"/>
214+ <arc id="P4_to_T2" source="P4" target="T2" type="normal">
215+ <inscription>
216+ <text>2</text>
217+ </inscription>
218+ <graphics>
219+ <position x="407" y="592"/>
220+ </graphics>
221+ </arc>
222+ <arc id="T1_to_P2" source="T1" target="P2" type="normal"/>
223+ <arc id="T0_to_P1" source="T0" target="P1" type="normal">
224+ <inscription>
225+ <text>2</text>
226+ </inscription>
227+ <graphics>
228+ <position x="375" y="282"/>
229+ </graphics>
230+ </arc>
231+ <arc id="T3_to_P7" source="T3" target="P7" type="normal"/>
232+ <arc id="T2_to_P4" source="T2" target="P4" type="normal">
233+ <inscription>
234+ <text>2</text>
235+ </inscription>
236+ <graphics>
237+ <position x="401" y="513"/>
238+ </graphics>
239+ </arc>
240+ <arc id="P1_to_T1" source="P1" target="T1" type="inhibitor"/>
241+ <arc id="P0_to_T0" source="P0" target="T0" type="inhibitor"/>
242+ <arc id="P5_to_T2" source="P5" target="T2" type="inhibitor"/>
243+ <arc id="P4_to_T3" source="P4" target="T3" type="inhibitor"/>
244+ </page>
245+ <name>
246+ <text>ComposedModel</text>
247+ </name>
248+ </net>
249+</pnml>
250
251=== added file 'test_models/inhibitor-relevance-test001/query.xml'
252--- test_models/inhibitor-relevance-test001/query.xml 1970-01-01 00:00:00 +0000
253+++ test_models/inhibitor-relevance-test001/query.xml 2021-10-12 10:06:40 +0000
254@@ -0,0 +1,36 @@
255+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
256+<property-set xmlns="http://tapaal.net/">
257+
258+ <property>
259+ <id>inhibitor-relevance-test001.FALSE-1</id>
260+ <description>inhibitor-relevance-test001.FALSE-1</description>
261+ <formula>
262+ <exists-path>
263+ <finally>
264+ <integer-eq>
265+ <tokens-count>
266+ <place>P2</place>
267+ </tokens-count>
268+ <integer-constant>1</integer-constant>
269+ </integer-eq>
270+ </finally>
271+ </exists-path>
272+ </formula>
273+ </property>
274+ <property>
275+ <id>inhibitor-relevance-test001.FALSE-2</id>
276+ <description>inhibitor-relevance-test001.FALSE-2</description>
277+ <formula>
278+ <exists-path>
279+ <finally>
280+ <integer-eq>
281+ <tokens-count>
282+ <place>P7</place>
283+ </tokens-count>
284+ <integer-constant>1</integer-constant>
285+ </integer-eq>
286+ </finally>
287+ </exists-path>
288+ </formula>
289+ </property>
290+</property-set>

Subscribers

People subscribed via source and target branches