5233 Commits (54c0bbb7c349c8f9558ad68230c8147081eae1c8)

Author SHA1 Message Date
Sebastian Junges 54c0bbb7c3 flatten of jani models before export via appropriate setting 7 years ago
Sebastian Junges e64e293d59 jani transformer which changes a variable into a location 7 years ago
Sebastian Junges f9e4208268 export jani with comment expressions to ease debugging jani models 7 years ago
Sebastian Junges 6275c52779 several convenience additions to jani data structures 7 years ago
Sebastian Junges 33c189bd32 export setting for flattening 7 years ago
TimQu 0c0f61e27b Fix: Only access counterexample settings in model-handling, if they are available. 7 years ago
TimQu 749ba87254 Made SVI log output more clear 7 years ago
Sebastian Junges 98969e627c updated counterexamples to support statistics to be exported 7 years ago
TimQu 1f6fc7e273 Better conversion of MA to CTMC if there are only Markovian states 7 years ago
TimQu 5a16b2befa minor fixes to let the total reward tests compile and pass 7 years ago
TimQu 1f4c0325be test cases for ctmcs and markov automata 7 years ago
TimQu 8df9b461cb total reward formulas for ctmcs and markov automata 7 years ago
TimQu b5566fa861 more on total reward formulas for mdps 7 years ago
TimQu b3edae8707 fixed fragment specification: total reward formulas should not be supported for hybrid/dd right now 7 years ago
Sebastian Junges 0be0126095 fixed support for highlevel counterex for expected rewards in dtmcs 7 years ago
TimQu c2dd57cda5 total rewards for mdps 7 years ago
TimQu 87e34d7b32 Added Support for Total Reward Formulas for DTMCs in the Sparse Engine 7 years ago
dehnert dfc0141894 minor fix to Z3 API modification 7 years ago
dehnert cdfa328464 first attempt at adapting to Z3 interface change 7 years ago
Matthias Volk afb0be1245 Fixed missing dependencies to storm-parsers 7 years ago
sjunges 8478352030 dynamic constraints and minimality labels 7 years ago
sjunges 53238f43f7 fixed some missing includes due to updated API 7 years ago
sjunges 39698d6ecb fix install of storm-counterexamples 7 years ago
sjunges 79bb6734ed compile and link parsers in seperate binary 7 years ago
sjunges 3a704ae532 fix storm-dft missing includes 7 years ago
sjunges 6dfce6a405 extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times 7 years ago
Sebastian Junges d1ab260068 remove outdated parts in highlevel counterexamplse 7 years ago
Sebastian Junges e29e6c7cd2 high level counterexamples extended with more options, and improved performance when minimizing over a subset 7 years ago
Joachim Klein b6d67e7995 properties.cpp: Output warning if we filter away all properties 7 years ago
Joachim Klein 2948611f3f cli.cpp: Quote arguments in "Command line arguments" status line 7 years ago
Joachim Klein 04a1bbedfc properties.cpp: Log filename of properties file in --verbose mode 7 years ago
Joachim Klein 30a95ef9d6 Simplify check whether argument of --prop is a file/property 7 years ago
Matthias Volk 99e5619952 Export storm targets 7 years ago
TimQu 1e4b81812c Environment does no longer require that unused setting modules still have to be registered. 7 years ago
TimQu 5c38a4ef89 implemented environment for multiobjective settings 7 years ago
dehnert e1bb35ca0f fix for the generator matrix fix 7 years ago
dehnert 62e493d978 fix computation of generator matrix, pointed out by jklein 7 years ago
dehnert ca651ec61c fixes github issue #24 related to MEC decomposition 7 years ago
dehnert 03707f0234 first step for fixing MEC decomposition: making SCC decomposition accept a bit vector of subsystem choices 7 years ago
Matthias Volk 2ba70e964c Added hasParameters() and supportsParameters() for symbolic models 7 years ago
Matthias Volk 6b91485382 Removed redundant file 7 years ago
Sebastian Junges f52aab0012 fixed out-of-bounds-labelling, added overlapping guards building, and some improved error messages if something goes wrong with highlevel counterex generation 7 years ago
Sebastian Junges 91bbe85a07 builder options for labeling overlapping guards 7 years ago
dehnert ceea5198d6 fixed detection of unreachability of target state in MaxSAT-based high-level counterexample generation 7 years ago
Sebastian Junges e7926b10c2 allow counterexamples for true jani models 7 years ago
Sebastian Junges c517ec14b1 support for liveness cex in jani 7 years ago
Sebastian Junges 0726dfc7a0 bugfix only add label out of bounds is option is set and state is present 7 years ago
Matthias Volk e6090d2d2c Removed unused code 7 years ago
Sebastian Junges 5b6383b5ef fix gspn export to pnml 7 years ago
Sebastian Junges 7a2a46cae9 fix warning about non-const comparison operator in set 7 years ago