This repository has been archived by the owner on Mar 13, 2024. It is now read-only.

Commits

Commits on Apr 12, 2018

adapted rersify to transform inside counting constraints
apirogov
committedApr 12, 2018

Commits on Sep 13, 2017

refactorings
apirogov
committedSep 13, 2017

Commits on Jun 8, 2017

rers solution check with spin OR flat-checker simplified graph, simplify'
apirogov
committedJun 8, 2017

Commits on Jun 5, 2017

added rers-related utilities and simple formula simplification
apirogov
committedJun 5, 2017

Commits on Jun 2, 2017

parse WU (weak until), sanity check of propositions in formula
apirogov
committedJun 2, 2017

Commits on May 31, 2017

splitting edges with cloned nodes, fixed counter resets with guards in last loop
apirogov
committedMay 31, 2017

Commits on May 13, 2017

add counter resets (e.g. x:=v)
apirogov
committedMay 13, 2017
extended parser to parse RERS challenge LTL almost without modifications
apirogov
committedMay 13, 2017

Commits on May 11, 2017

refactorings, added some sanity checks, prepare for benchmarking stuff
apirogov
committedMay 11, 2017

Commits on May 3, 2017

hopefully fixed formula for infinite loop labelling cases
apirogov
committedMay 3, 2017

Commits on Apr 23, 2017

minor cosmetics
apirogov
committedApr 23, 2017

Commits on Mar 31, 2017

fix edge upd/grd and formula parsing bug, remove {}, add -s and -d flags, add version information
apirogov
committedMar 31, 2017

Commits on Jan 22, 2017

big update. allow DNF constraints in graph, allow linear constraints in formulas, automatic minimal run search with -m
apirogov
committedJan 22, 2017

Commits on Jan 18, 2017

bumped stackage, added some missing top level types, fixed/improved doc.
apirogov
committedJan 18, 2017

Commits on Dec 18, 2016

improved parsing: formulas can have optional parentheses, propositions can be strings, graph annotation is more liberal
Anton Pirogov
committedDec 18, 2016

Commits on Dec 13, 2016

another try to fix U[r], better counter pretty printing
Anton Pirogov
committedDec 13, 2016
replaced pairs of complementary implies with ite
Anton Pirogov
committedDec 13, 2016

Commits on Dec 12, 2016

Added line numbers on the left, hopefully fixed U[r] ?
Anton Pirogov
committedDec 12, 2016
fixed broken normal until
Anton Pirogov
committedDec 12, 2016
input graph now can have linear guards and constant updates for counters
Anton Pirogov
committedDec 12, 2016

Commits on Dec 11, 2016

generalized types, implemented parsing of guards and updates from graph labels
Anton Pirogov
committedDec 11, 2016
removed custom graph format, keeping only dot input
Anton Pirogov
committedDec 11, 2016
generalized LoopType 2-boolean enum to general bit-blasted enums
Anton Pirogov
committedDec 11, 2016
tried to encode dynamic run size in Z3. did not work well. useless without some Z3 tactics
Anton Pirogov
committedDec 11, 2016

Commits on Dec 10, 2016

fused type of LT and Nid enums to a EnumAPI existential
Anton Pirogov
committedDec 10, 2016

Commits on Dec 9, 2016

some refactoring etc.
Anton Pirogov
committedDec 9, 2016
evil until is done
Anton Pirogov
committedDec 9, 2016

Commits on Dec 7, 2016

fixed a lot of warnings, parametrized guards, calc loop delta
Anton Pirogov
committedDec 7, 2016

Commits on Dec 6, 2016

Implemented Johnson algorithm, some refactorings, added -l flag
Anton Pirogov
committedDec 6, 2016

Commits on Nov 27, 2016

ignore empty lines
Anton Pirogov
committedNov 27, 2016

Commits on Nov 26, 2016

added .dot file support
Anton Pirogov
committedNov 26, 2016
small fix
Anton Pirogov
committedNov 26, 2016

Commits on Nov 25, 2016

added counters, guards and updates. left to do: correct U[m/n] labelling
Anton Pirogov
committedNov 25, 2016

Commits on Nov 23, 2016

make use of -v flag, add comments to graph file
Anton Pirogov
committedNov 23, 2016
fixed args parsing of -g
Anton Pirogov
committedNov 23, 2016