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

Branch merges

Propose for merging

No branches dependent on this one.

Merged into lp:verifypn at revision 255

VerifyPN Maintainers: Pending requested 2021-10-12

Diff: 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)

api

Related source package recipes

No recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related bugs

Related blueprints

254. By Jesper Adriaan Van Diepen on 2021-10-12

Actually added the mentioned test model this time.

253. By Jesper Adriaan Van Diepen on 2021-10-12

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.

252. By Jesper Adriaan Van Diepen on 2021-10-12

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.
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.

251. By Jiri Srba <email address hidden> on 2021-09-01

merged in lp:~yrke/verifypn/fixed-required-bison-version updateing cmake scripts for bison

250. By Jiri Srba on 2021-08-21

merged in lp:~tapaal-ltl/verifypn/kbound-fix-ltl fixing problem with k-bound and A true in LTL engine

249. By Jiri Srba <email address hidden> on 2021-08-19

merged in lp:~tapaal-contributor/verifypn/Fix-partition-id-clash-1939939 fixing id clashes under unfolding

248. By Jiri Srba on 2021-08-18

merged in lp:~tapaal-ltl/verifypn/fireable-empty-preset-fix fixing fireability predicate for transitions with empty preset

247. By Jiri Srba <email address hidden> on 2021-08-09

merged in lp:~tapaal-ltl/verifypn/ltl-trace-fixes fixing trace generation and replay

246. By Jiri Srba on 2021-08-05

merged in lp:~tapaal-ltl/verifypn/ltl-spring-2021 adding many additions to LTL model checker (automata based methods for partial order and heuristic) and trace generation

245. By <email address hidden> on 2021-07-18

merged in lp:~tapaal-contributor/verifypn/Fix-partitioning-1934103 fixing issue with unfolding