sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Commit Graph

  • 75b6ac27e8 JaniParser: Making result field optional (fixes #83) Tim Quatmann 2020-12-01 14:59:26 +0100
  • 3184ba1611 Jani: Correctly parse the input-enable field. Throw an error in the sparse model builder, as these are not supported right now. Tim Quatmann 2020-12-01 14:51:55 +0100
  • 41ae9d5624 Fixed silently truncating bits when parsing integer literal expressions (see https://github.com/moves-rwth/stormpy/issues/20) Tim Quatmann 2020-11-30 11:48:35 +0100
  • 6cea196953 rpatl smg formulas now accept operatorFormulas Stefan Pranger 2020-11-24 16:05:13 +0100
  • 51f86db9eb Storm version 1.6.3 Tim Quatmann 2020-11-24 12:48:07 +0100
  • 7002946845 Updated changelog. Tim Quatmann 2020-11-24 10:10:55 +0100
  • 251527bccf storm-pars: Make a more explicit warning if a non-parametric equation solver type is selected. Tim Quatmann 2020-11-24 10:09:09 +0100
  • 1243feba8c Substitute constants in JANI Properties (fixes #95) Tim Quatmann 2020-11-23 22:01:38 +0100
  • a9868fd501 refactor Coalition to use boost variant Stefan Pranger 2020-11-23 18:09:24 +0100
  • 84bcfef24e removed print from CloneVisitor Stefan Pranger 2020-11-23 17:49:12 +0100
  • 2fb1f36fda Merge branch 'keep-module-index-map-in-parsing' into game_formula_parsing Stefan Pranger 2020-11-23 17:17:28 +0100
  • 53ac9a3873 fixed typo in arg list of GameFormula Stefan Pranger 2020-11-23 13:45:16 +0100
  • 376e4756db added Coalition default ctor Stefan Pranger 2020-11-23 13:44:46 +0100
  • 73e4945818 add STORM_DEVELOPER ALL_WARNINGS GCC case Stefan Pranger 2020-11-23 13:20:46 +0100
  • f106b83328 WIP added grammar rules for gameFormula Stefan Pranger 2020-11-19 18:23:32 +0100
  • 715784a070 added casting getter for gameFormula Stefan Pranger 2020-11-19 18:26:42 +0100
  • 8dc46968cb added rPATL to FragmentSpecifitcations Stefan Pranger 2020-11-19 18:11:20 +0100
  • c52fcba6a2 added multiple Visitor methods for gameFormulas Stefan Pranger 2020-11-19 18:08:51 +0100
  • 6dd9e09ede added GameFormula class Stefan Pranger 2020-11-19 18:12:54 +0100
  • cbbafaddfd added Coalition class Stefan Pranger 2020-11-19 18:13:20 +0100
  • 2225ebcbe8 fix reorder warning Stefan Pranger 2020-11-23 14:25:35 +0100
  • eba20bb005 switch cases in engine now feature SMG case Stefan Pranger 2020-11-23 14:24:48 +0100
  • 065b366198 Removed superfluous '.' in output of Markov automata model data. Tim Quatmann 2020-11-23 10:37:51 +0100
  • 6d6e142236 Fixed an issue with JANI models concerning properties using transient variable expressions. Tim Quatmann 2020-11-20 12:25:29 +0100
  • ee5fff680a Indefinite Horizon helpers: Do not compute values of MaybeStates if they are not relevant for the property. (Fixes #87) Tim Quatmann 2020-11-20 10:35:02 +0100
  • 20d424e289 JaniTraverser: Only traverse lower/upper bound expressions of BoundedIntegerVariables, if these bounds exists. Tim Quatmann 2020-11-20 09:36:59 +0100
  • ce0283d80d Cmake: checked whether the stack-check issue still persists with current AppleClang v12.0.0 Tim Quatmann 2020-11-20 09:35:57 +0100
  • 8619a4d833 CMake: Implemented a workaround for building CUDD on MacOS Big Sur. Tim Quatmann 2020-11-19 17:31:29 +0100
  • 1982dc0dba SparsePcaaParetoQuery: Added a (hopefully explaining) comment Tim Quatmann 2020-11-19 17:29:28 +0100
  • 6a71c19d8a added sparse smg model Stefan Pranger 2020-10-25 12:57:25 +0100
  • bb05b9c03c aggregate player indices into model Stefan Pranger 2020-08-19 12:04:51 +0200
  • cea09f932b generator now assigns player indices to states Stefan Pranger 2020-08-19 12:02:39 +0200
  • 163dfa8654 ModelComponents now feature a player mapping Stefan Pranger 2020-08-19 11:59:25 +0200
  • 6b715792aa added player related helpers Stefan Pranger 2020-08-19 11:54:46 +0200
  • 160a2c32a2 added SMGs to existing ModelTypes Stefan Pranger 2020-08-17 14:51:19 +0200
  • dce9496300 Model validity check now handles SMGs Stefan Pranger 2020-08-17 14:42:52 +0200
  • 9bf2a572a7 check if state is controlled by multiple players Stefan Pranger 2020-08-13 22:08:03 +0200
  • e9a6077acb adapted player ostream output Stefan Pranger 2020-08-13 21:00:13 +0200
  • 1cf2e544ac add assertion for module indices in second Stefan Pranger 2020-08-13 18:49:53 +0200
  • de301323d6 check module and action names when parsing players Stefan Pranger 2020-08-13 11:39:40 +0200
  • 43353d5243 store name index map for player member Stefan Pranger 2020-08-13 11:38:26 +0200
  • 271ed284a6 fix player ostream output Stefan Pranger 2020-08-13 09:12:50 +0200
  • 11f7464372 players now get stored in PRISM programs Stefan Pranger 2020-08-13 09:12:35 +0200
  • 48276e47a9 further work on player parsing Stefan Pranger 2020-08-12 14:22:11 +0200
  • 3f3b154ce0 first progress on player parsing Stefan Pranger 2020-08-12 10:37:43 +0200
  • 55f4efd40a added SMG ModelType Stefan Pranger 2020-08-11 16:33:38 +0200
  • bf54ca8a52 init Player class for SMG parsing Stefan Pranger 2020-08-11 16:33:05 +0200
  • d35e9a6a40 removed plenty of empty line whitespaces Stefan Pranger 2020-08-11 16:32:32 +0200
  • c12c0352f7
         Support for parsing jani model from string Matthias Volk 2020-11-10 16:52:28 +0100
  • 209090eb93
         storm-dft: Ignore compound nodes in json parser Matthias Volk 2020-11-03 10:40:31 +0100
  • d0c153da8d Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs) Tim Quatmann 2020-10-23 17:41:05 +0200
  • 9775964f43 Pcaa: Fixed unnecessary insertion of diagonal entries in deterministic transitions. Tim Quatmann 2020-10-23 15:30:48 +0200
  • 3a4af89b66 graph: Cycle check ignores Zero entries. Tim Quatmann 2020-10-23 15:25:51 +0200
  • d53cffab08 avoid resize that caused unstable behavior Sebastian Junges 2020-10-22 22:26:32 -0700
  • f7d75b1677 Merge remote-tracking branch 'refs/remotes/origin/master' Tim Quatmann 2020-10-22 17:50:36 +0200
  • 2cadf3a252 Added support for generating optimal schedulers for globally formulae Tim Quatmann 2020-10-22 17:39:23 +0200
  • f5ce4860ac Updated changelog. Tim Quatmann 2020-10-22 17:38:17 +0200
  • 4ffe13063c Fixed the offline_package.md documentation to incorporate more recent changes in Storm. Tim Quatmann 2020-10-22 15:56:48 +0200
  • dc8612b751 Fixed not always using the acyclic solver within LRA and multi-objective time-bounded reachability computations. Tim Quatmann 2020-10-22 15:55:56 +0200
  • 8b05837e77
         Fixed assertion for RationalFunction Matthias Volk 2020-10-21 10:09:45 +0200
  • dced2bb9b6 Merge branch 'master' into rubicon Sebastian Junges 2020-10-20 14:55:12 -0700
  • 32c88825e2 cleanup Sebastian Junges 2020-10-20 14:07:24 -0700
  • 50a82c1127 Merge branch 'master' into monitoring Sebastian Junges 2020-10-20 11:49:05 -0700
  • 664484883a allow termination in inner loop of OVI Sebastian Junges 2020-10-20 11:48:23 -0700
  • c247b4ab55 fixed type in offline_package documentation Tim Quatmann 2020-10-19 15:33:17 +0200
  • 90e1eeba28 Merge branch 'multi-objective-lra' TimQu 2020-10-16 13:13:32 +0200
  • 9d29f369e2 fixed incorrect hanlding of lra objecties in bounded phase Tim Quatmann 2020-10-16 13:12:40 +0200
  • 9a8f40bb33 Multi-obj preprocessor: Fixed an issue when preprocessing LRA operator formulas Tim Quatmann 2020-10-14 14:45:27 +0200
  • 6dcbf75fe3
         Update progress measurments only if --progress flag is set Matthias Volk 2020-10-08 11:47:08 +0200
  • 27cb582243 MDP Instantiation model checker: Fixed setting model checking hint information. TimQu 2020-10-06 21:39:22 +0200
  • 5213be9b69 More statistics output. Tim Quatmann 2020-10-02 17:15:25 +0200
  • 20665eb862 multi-objective: Aborting time-bounded reachability computation when termination signal is received. Tim Quatmann 2020-10-02 12:48:35 +0200
  • c1c0fcf8f3 Display a bit more statistics for multi-objective model checking. Tim Quatmann 2020-10-02 12:37:26 +0200
  • ce14b45578 Pcaa: Implemented termination signal. Tim Quatmann 2020-10-02 12:09:42 +0200
  • b6259e7ea3 SparseMaPcaaTest: Temporarily disabled a test as it did contain non-optimal points due to numerical issues. TimQu 2020-10-01 20:03:58 +0200
  • ce962bf1df SparseMaPcaaChecker: Fixed cycle detection. TimQu 2020-10-01 20:03:15 +0200
  • 5a6952899b MaPcaaWeightVectorChecker now uses the acyclic solver if possible. Tim Quatmann 2020-10-01 15:51:31 +0200
  • 5e9241fcd1 Allowing reward accumulations in multi-objective model checking queries. Tim Quatmann 2020-10-01 15:51:07 +0200
  • da6333cead Fix in scheduler export for acyclic Min Max solver Tim Quatmann 2020-10-01 15:50:38 +0200
  • e513a3fb62 progress in monitoring with timeouts etc Sebastian Junges 2020-10-01 00:24:52 -0700
  • 4760a12815 reset signal handler Sebastian Junges 2020-10-01 00:23:47 -0700
  • f9ee3d10e4 simulating with rationals Sebastian Junges 2020-10-01 00:23:22 -0700
  • b7ad55b34b random prob generator for rationals Sebastian Junges 2020-09-30 20:31:54 -0700
  • b45497a8c4 Added --propsasmulti switch to interpret input formulas as multi-objective formula TimQu 2020-09-30 22:00:10 +0200
  • 2aab7f99db Merge branch 'master' into multi-objective-lra Tim Quatmann 2020-09-30 15:02:34 +0200
  • 260c14a3f6 ExpressionParser: Allow sequences of unary operators, like '!!x=0' (fixes #89) Tim Quatmann 2020-09-30 13:54:18 +0200
  • 16ecb0fc8d OVI: display current number of iterations with --progress --verbose. Tim Quatmann 2020-09-30 13:53:15 +0200
  • bd3c42561b Added multi-objective lra test case for MA Tim Quatmann 2020-09-29 14:02:59 +0200
  • 97d4dba540 Added test case for Multi-objective LRA combined with step-bounded property. Tim Quatmann 2020-09-29 14:02:37 +0200
  • c990d27c50 Added MA test case + fixes Tim Quatmann 2020-09-29 13:22:48 +0200
  • 5bfb3b132e New MDP LRA Test case + fix Tim Quatmann 2020-09-29 11:42:17 +0200
  • 7023736e3d Added resource-gathering testfile Tim Quatmann 2020-09-29 09:17:07 +0200
  • ee06a1f1a6 Also added test case for lra operator formula. Tim Quatmann 2020-09-28 19:29:47 +0200
  • 6154bd39f9 Fixes for new test case. Tim Quatmann 2020-09-28 19:22:59 +0200
  • 3789fbb3e9 Test case for multi-objective lra Tim Quatmann 2020-09-28 19:22:48 +0200
  • 07f7ce7963 Merge branch 'master' into multi-objective-lra TimQu 2020-09-28 11:12:50 +0200
  • f100ff6275 LraViHelper: Fixed unordered insertion into SparseMatrixBuilder. TimQu 2020-09-28 11:12:38 +0200
  • 36f27e4391 Added a simple example model for multi-objective lra. TimQu 2020-09-25 23:25:44 +0200
  • 139c86f6a0 Fixes for multi-obj LRA TimQu 2020-09-25 23:24:42 +0200
  • 400b69663a Fixed multi-obj. tests TimQu 2020-09-25 21:26:32 +0200