6285 Commits (cd5b805a761d729da12bad214a90522c3b4e6dbe)
 

Author SHA1 Message Date
TimQu cd5b805a76 Under- and overapproximation for Pareto curve check result are now optional 7 years ago
TimQu b748b27b85 fixed compilation of settings... 7 years ago
TimQu b14c554df2 correct treatment of Markov Automata in scheduler evaluator 7 years ago
TimQu a73574a99f added functionality to translate a polytope to an expression 7 years ago
TimQu f1eaab5603 enabling preservation of total reward formulas in ContinuousToDiscreteTimeModelTransformer 7 years ago
TimQu 0e70cfc617 added setting to print intermediate results during the computation 7 years ago
TimQu 789367a28b using new memory incorporation in multi objective model checking 7 years ago
TimQu d24d1bdcd8 added memory incorporation transformer 7 years ago
TimQu 5163803243 added nondeterministic memory structure 7 years ago
TimQu 51a5a82a5f more functionality for deterministic Pareto Explorer 7 years ago
TimQu 7b43e79ff5 adding missing template instantiation 7 years ago
TimQu 5f8af5a38a added coordinate utility file 7 years ago
TimQu 80da98eec5 adding shift method to polytope interface 7 years ago
TimQu b075c16ce0 Merge branch 'master' into deterministicScheds 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
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
TimQu e4817759df policy iteration based weight vector checker 7 years ago
TimQu aece3020f6 improved functionality of the scheduler evaluator 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
TimQu bf973187c4 use deterministicParetoExplorer in case there is a scheduler restriction. 7 years ago
TimQu a638104adb using new post processing class for the 'old' implementation. 7 years ago
TimQu 80a66603fb added possibility to compute the 'downward closure' of a polytope only with respect to a set of dimensions 7 years ago
TimQu 136084af75 started implementing deterministic scheduler finding approach for multi-objective model checking 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 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
TimQu 918dc349fb Multi-objective tests now set the method via the environment 7 years ago
TimQu 7cee81a223 adapt multi-objective model checking components to new preprocessing 7 years ago
TimQu 4c0bda2664 better modularity for multi-objective preprocessing 7 years ago