6885 Commits (230ac204807619277381c366e5eae29bd33e647d)
 

Author SHA1 Message Date
Matthias Volk 48efde755b DFT: export to JSON as string 7 years ago
Matthias Volk 369d106f99 DFT: load json from string 7 years ago
Matthias Volk 856d62513b DFT: parse number from JSON 7 years ago
Matthias Volk cbd709f0cd Fixed assertion 7 years ago
Sebastian Junges a34ca5c9ac dont go on as soon as trivial command set is necessary 7 years ago
Sebastian Junges 73900f1bbe advanced stopping criteria for multi-counterexamples, additional measurements for cuts, an option to properly disable backward implications, and some cleaning 7 years ago
Sebastian Junges ac9d9d6778 fix in counterexamples for lower bounds that was recently introduced 7 years ago
Sebastian Junges 919dfeebae "number of edges" and "number of commands" in jani model / prism programs 7 years ago
TimQu a21c6f7244 fixed wrong state action rewards in JaniNextStateGenerator. 7 years ago
TimQu d8bc689259 Throw an exception instead of assertion when 'wrong' jani was detected 7 years ago
TimQu 0332935451 Supporting TimeOperatorFormulas for MDPs and DTMCs in Sparse, Hybrid, and Dd engine 7 years ago
Joachim Klein d0e2d099bf AbstractModelChecker: In error messages, include class name of the actual model checker 7 years ago
Joachim Klein da4dfc35a8 AbstractModelChecker: add getClassName() 7 years ago
TimQu ed2de09ce3 added function that reduces the nesting of expressions (e.g. when considering a big sum with many summands. This fixes stack overflows when translating expressions 7 years ago
TimQu 6449dee626 fixed typo 7 years ago
TimQu e7eb80184e fixed wrong include.. 7 years ago
Matthias Volk c9cea88047 Export Storm-gspn headers as well 7 years ago
TimQu 910b6e6b22 fixed wrong include 7 years ago
TimQu b3be56588f fixing time operator formulas 7 years ago
TimQu 066facf3f1 fixed respecting the --globalvars option correctly... 7 years ago
TimQu 611428c01f allowing constants in property bounds 7 years ago
TimQu 9487223dc1 --globalvars option no longer requires a module prefix 7 years ago
TimQu b4a1244d01 correct parsing of bounded until formulas with multiple bounds 7 years ago
TimQu 56a5dcf7cb added setting in storm-conv to make variables global 7 years ago
TimQu 5937131ff2 fixed and extended parsing of jani formulas with Emin or Emax operator 7 years ago
TimQu fe71dfdf9b added export of reward-bounded until formulas 7 years ago
TimQu 01549dfdea fixed segfaults when lifting transient destination assignments to the edge 7 years ago
TimQu 8f179217d0 fixes for storm-dft and storm-gspn 7 years ago
TimQu 52fc8c8e35 removed unused setting 7 years ago
TimQu 41645c3f9a including the correct .h file in storm-parsers api 7 years ago
TimQu 9563cb44cb made storm-pgcl use storm-conv 7 years ago
TimQu d9ec0f8fcf removed include of old janiexportsettings 7 years ago
TimQu f0d11afdb8 fixed compilation of tests 7 years ago
TimQu 4a7a82627f storm-gspn and storm-dft now use functionalities of storm-conv 7 years ago
TimQu c268926568 storm-pars no longer uses export settings 7 years ago
TimQu 30d30a063c setting jani conversion options from settings 7 years ago
TimQu 51c5c42319 Fixed export of expected time properties to jani 7 years ago
TimQu 0fa361c393 displaying property name together with the property 7 years ago
TimQu d343943cbd storm-conv should not fail if no input arguments were given 7 years ago
TimQu 636d92894c Fixed an issue with time bounded properties specified in jani 7 years ago
TimQu 31efde52c2 fixed case where no location variables were provided 7 years ago
TimQu 35aa166f5b added possibility to check all available jani properties 7 years ago
TimQu a4864f3c3d Using JaniExportSettings in storm-conv 7 years ago
TimQu fbb734fbe2 Fixed using settings without the 'general' module 7 years ago
TimQu 86f0195b18 removed jani conversion in cli of main binary 7 years ago
TimQu e5e6e1bd79 worked on prism to jani converter 7 years ago
TimQu 2e035f3957 started working on conversion binary 7 years ago
Alexander Bork a8d4c45299 Reworked extended priority computation 7 years ago
TimQu db72a05358 fixed log output 7 years ago
Sebastian Junges 6051363782 initial support for multi-reward structures in counterexample generation 7 years ago