Unify parsing with unfoldTACPN #42
Labels
enhancement
New feature or request
Comments
petergjoel
pushed a commit
to TAPAAL-Developers/verifypn
that referenced
this issue
Apr 28, 2022
…PAAL#42) Fixes pnmlwriter, such that it can better handle all-expressions, and find color for places
petergjoel
added a commit
to TAPAAL-Developers/verifypn
that referenced
this issue
May 1, 2022
* enabled newline printing * update help to reflect actual options * printing help on no options, fixing argument for --disable-partial-order in parsing * fixing option formatting * updated scripts * added missing variable * fixed firecount heuristics * Rename POR options switches, purge mixed options * more testing friendly * moving simplification out to own function * added games to the model * refactoring code to avoid linker issue * Added CTL* syntax, plus some of the special MCC syntax * fixes from comments * fixed error in test * added control condition * removing unused method * Added proper precendence to rules * handling control in the visitors * added positioning for unfolding * disabeling reductions in the pressence of games * disallowing reductions * update positioning * trying to make builds work on windows again * added default/failing handing of synthesis * added exit when reductions are used with synthesis * snapshot, adding synthesis, incomplete * Update ColoredPetriNetBuilder.cpp * compiles * started tests * added a few simple tests * fixed paths of tests * added testing * fix PR comments * correcting tests * updating ltl-por argument to reflect new naming * refactoring and adding search strategies * Fixing BFS * decomposing code * more restructuring * fixed translation into CTL * adding output * trying to remove flto to make windows compile * Revert "trying to remove flto to make windows compile" This reverts commit 33abde3. * refactoring structures out of main code-base * more refactoring * dummy implementation of POR * starting POR, refactoring out successor-generator for games for a cleaner interface * adding new test-case * added missing files * restructured a bit * compute all enabled even if an unsafe is added. * fixed code for now * added *some* future approximation, full version still to come * light refactor * trying some dependency * added future approximation also for adding to stubborn set (only add things that can be enabled in the future) * added bounds computation for more accurate forward approximation * removed redundant option * adding interval visitor * added overapprox for compareconjunction * added deadlock check also * added comment * fixed evaluation and missing indexing * fixed trace abstraction option * fixes build issues on windows * fixing warnings * should fix windows linking issues * Fixed isReachability checker, visitor now checks for not reachability to fit the 'any' visitor. * BOOST_ASSERT -> BOOST_TEST * Removed error term to avoid infinite error loop * Changed multiple argument is-fireable to disjunction * type-check on marking * added test-case * Fixed memory access issue in eq-class-vector * moved is-fireable interpreted as disjunction, fixed test * exit to exception * adding ctrl condition to pql parser * changed to a more liberal parser * split tests * simplified query parsing * Fixed test errors * fixed single argument is-fireable * added extra test-case for long & mixed properties * Moved analyze to visitor * Update README.md mac compilation details * removed 'ERROR:' from exception and addded try/catch in main * Moved constraint into simplifier and changed it to visitor pattern * minor fix * merge conflicts * Evaluate to visitor * Eval and set to visitor * Fixed isReachability tests * not reachability when note compiled * added output of empty trace when proposition is solved in initial marking + output when solved by TAR * change initial marking datatype and checks * Change PTBuilder token type * outputting queries before any reduction/solving * Fixed minor error * change initial marking to 64 bit * added failing test * fixing type (using place-id instead of weight on arc) and tightening forward approximation. Both affecting POR for games. * cast to base instead of re-visit * snapshot * added comment * migrating into a direct-jump visitor-pattern * finishing visitor pattern * simplifying flow * missed setEval * math is hard * enabled ltl eval * full specified name * migrating LTL to new visitor (inheriting from old) * completed migration to new visitor pattern * Siphon Traph Output Also output "Solved by Siphon-Trap" for AG * adding missing default visitor for shallow identifier * purging un-needed maps * simplifying more * Fixed issue where <?xml tag was included in trace output * fixed default init * direct translation of spot formula instead * trying translating to atomics * changing printing * fixing out streams * more on outstreams * Hacking traces for AG being true in initial state * fixed false approximation happening w. new initial marking-check * simplifying AST * adding forced solved query output for GUI * no unfolding in simplification * added special case for orphaned places (by color) * fixed wrong dual treatment of < * removed ebug * adding visitor pattern * chaging toString into visitor * improved printing (added preceedence) and added missing out of UserOperator * removed unused methods * migrating color eval to visitor * moved symmetry check to visitor * simplifying/hiding getColorType * slight refactor * moving OutputInterval check into visitor * fixing regression * faster * migrating more into visitors * added missing index reset * fixed wrong pred/succ computation * fixing refactor errors * moved out last part of expression analysis into visitor * added missing file * moving stable computation out * moving colored fixed point out * fixing typo * added missing initialization * reorder * moved symmetry-visitor out * structures is in place * handling uncolored * added failing tests * fixingt defaults * fixing issue w. wrong initialization of partition when partitioning is disabled * fixing test and handling of stripping of colors * fixes issue with unfolding UtilityControlRoom-COL-Z2T3N04 * added model failing in unfolding prior to da42623 * added failing test * fixing issue with NeoElection * reenabled tests * another go at testing * correct version of boost * file-paths are hard, yo. Co-authored-by: pgj <[email protected]> Co-authored-by: srba <[email protected]> Co-authored-by: Nikolaj Jensen Ulrik <[email protected]> Co-authored-by: Ragusaen <[email protected]> Co-authored-by: Peter Gjøl Jensen <[email protected]> Co-authored-by: Rasmus Tollund <[email protected]> Co-authored-by: MathiasMehl <[email protected]> Co-authored-by: Kenneth Yrke Jørgensen <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Lots of the functionality of the parser and unfolder is dupplicated in the unfoldTACPN library.
Ideally we should migrate the key functionality that can be shared of parsing into unfoldTACPN to create a unified library for parsing both queries and petri-nets.
The parsingspeed of unfoldTACPN needs to be studied to make sure that we don't regress on performance on very large petri-nets.
The text was updated successfully, but these errors were encountered: