6361 Commits (3e8959c8666932eb4381748a7d5ea5ccbee4058a)
 

Author SHA1 Message Date
dehnert 50aa6d1424 assuming the only global real transient variable is the reward when exporting JANI and no reward model is mentioned in the property (issues a warning) 7 years ago
dehnert c4bed85dc4 switching to native linear equation solver by default and power iteration 7 years ago
TimQu 1f6fc7e273 Better conversion of MA to CTMC if there are only Markovian states 7 years ago
TimQu ca2295be1d updated changelog: support for expected total rewards 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
Sebastian Junges 73a1911a53 Merge branch 'master' into counterexample_improvements 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 a6e6d5993f Travis: set unlimited clone depth to allow versioning with git describe 7 years ago
Matthias Volk afb0be1245 Fixed missing dependencies to storm-parsers 7 years ago
Matthias Volk 9e398ffaab Minor improvements for some CMake output 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
sjunges 6fcc91b9d0 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm 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
sjunges ade4b5bf72 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm 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 a2c990ea58 Travis: changed mail address for notifications 7 years ago
Matthias Volk c5e356bc40 Proper installation of Storm 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
dehnert 94a5a3da7c remove ffast-math 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