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

Commit Graph

  • 1649d47d66 Renamed lower/upper bounds to under/over approximation in weightVectorCheckers TimQu 2017-05-03 19:20:56 +0200
  • aa4d2141c3 build infrastructure for switching between multi objective model checking methods TimQu 2017-05-03 18:38:16 +0200
  • 7dd5c9e2c5 actually fixed the issue with timed reachability TimQu 2017-05-03 16:41:44 +0200
  • c2f21e007e fix that correctly sets the lower and upper bounds for multi-objective timed reachability TimQu 2017-05-03 16:16:24 +0200
  • 725e0e12e7 replaced old pcaa preprocessor with the refactored preprocessor. TimQu 2017-05-03 00:49:15 +0200
  • ef90b1b224 Fix for memory structure product and toString method TimQu 2017-05-03 00:35:20 +0200
  • cdb923403f Improved and fixed multiObjectivePreprocessor TimQu 2017-05-03 00:34:39 +0200
  • 6598ade4ac fix for getting the choices with zero reward TimQu 2017-05-03 00:31:55 +0200
  • e8adc21fdb version is now updated to a dev version when committing after a tagged version Sebastian Junges 2017-05-02 17:52:07 +0200
  • 5c39065758 fixes for new goal state merger TimQu 2017-05-02 10:18:41 +0200
  • 7833975e46 Merge remote-tracking branch 'origin/master' into smt-based-multi-objective TimQu 2017-04-30 15:00:17 +0200
  • 2ae264f176 Merge branch 'master' into smt-based-multi-objective TimQu 2017-04-30 14:59:36 +0200
  • ee54c6cdac Towards refactoring multi-objective preprocessing TimQu 2017-04-30 14:59:03 +0200
  • 6d86df0ead fixed doing the end component analysis in multi objective model checking multiple times TimQu 2017-04-30 14:50:16 +0200
  • b6d085a92d fixes and improvements for the new goal state merger TimQu 2017-04-30 14:46:52 +0200
  • 2931436201 added utility functions for end component analysis TimQu 2017-04-30 14:46:13 +0200
  • a887fd9224 added possibiliy to perfromProbGreater0A only for a selected set of choices TimQu 2017-04-30 14:44:51 +0200
  • c14213f9a6 Reward model can now retrieve the set of choices with zero reward TimQu 2017-04-30 14:40:21 +0200
  • 7234ffe5e7 Merge remote-tracking branch 'origin/master' into jani_next_state_generator dehnert 2017-04-29 10:50:40 +0200
  • b2b692b8ae extended JANI next-state generator to be able to deal with custom system compositions dehnert 2017-04-29 10:50:30 +0200
  • a2ed0fc4bf item labelling class Sebastian Junges 2017-04-28 11:54:06 +0200
  • ed2a1dc1de CMake now ensures that carl is not only configured, but also built and thereby prevents compilation-time errors. Sebastian Junges 2017-04-27 23:46:02 +0200
  • 0b2a8d1adf fixed comments and names of arguments in file.h for consistency Sebastian Junges 2017-04-27 21:08:21 +0200
  • 920d48c2bd storm config version now also correctly exported Sebastian Junges 2017-04-27 20:42:42 +0200
  • 492debf017 added two elements to changelog dehnert 2017-04-27 20:39:37 +0200
  • a21e9d4ca8 changelog Sebastian Junges 2017-04-27 18:13:45 +0200
  • 7a40af2b98 storm version is now exported Sebastian Junges 2017-04-27 18:07:30 +0200
  • 48957978eb Extended Functionality of goal state merger TimQu 2017-04-27 17:00:18 +0200
  • ee185d2717 Export options whether CLN is used. Sebastian Junges 2017-04-27 16:58:45 +0200
  • 92f04cdfa1 CppTemplate was not correctly listed as a dependency of storm. Sebastian Junges 2017-04-26 15:03:31 +0200
  • d94c66fcaa fixed: Nofixdl was always set in JIT Sebastian Junges 2017-04-26 13:48:29 +0200
  • dd647e93d2 Merge branch 'master' into smt-based-multi-objective TimQu 2017-04-26 11:15:43 +0200
  • b7aaf1957e Replaced the StateDuplicator with the new memory structure product TimQu 2017-04-26 11:15:14 +0200
  • c5f29c3761 Fixes and improvements for memory structure TimQu 2017-04-26 10:54:47 +0200
  • 524efc616d Jit-builder now gives better diagnostics when nofixdl option is set. Sebastian Junges 2017-04-25 19:45:26 +0200
  • 6a3310f7ee Improved Jani-to-dot: Sebastian Junges 2017-04-25 18:15:33 +0200
  • 291f5ecd47 First version of Jani-to-Dot. Sebastian Junges 2017-04-25 16:26:15 +0200
  • 6c8d2a31fc Better error messages when something is wrong with the argument given. Sebastian Junges 2017-04-25 16:10:32 +0200
  • 697ae21b6f Suppress warning Sebastian Junges 2017-04-25 15:44:17 +0200
  • 586929ea64 As we do not support windows, we can also get rid of: Sebastian Junges 2017-04-24 13:27:19 +0200
  • 5f120fd5bb Fixed enabling CLN when there is no system version of carl TimQu 2017-04-25 17:36:37 +0200
  • fc97c1fc9d introduced memory structure TimQu 2017-04-25 17:35:57 +0200
  • 194015bcd4 PLA: display number of corrected regions when doing exact validation TimQu 2017-04-23 13:50:18 +0200
  • 3f9aa29db2 Fixed compilation with gmp as rationalNumber/ rationalFunctionCoefficient TimQu 2017-04-21 19:47:54 +0200
  • 1e3e54ef51 Merge remote-tracking branch 'origin/master' into symbolic_bisimulation dehnert 2017-04-20 22:15:14 +0200
  • 28e91b8d0f more work on symbolic bisimulation dehnert 2017-04-20 22:15:01 +0200
  • 43fdf0a89b Fixed a couple of warnings TimQu 2017-04-20 17:05:25 +0200
  • 1860e889d6 Merge branch 'refactor_pla' TimQu 2017-04-19 19:03:05 +0200
  • 511fe90c5b Merge branch 'master' into refactor_pla TimQu 2017-04-19 18:55:17 +0200
  • 5e9642c1fa conversion of symbolic state-action rewards is not supported at this point TimQu 2017-04-19 18:55:10 +0200
  • 03ad4c2783 first version of symbolic bisimulation minimization dehnert 2017-04-19 18:24:47 +0200
  • 5f83f4451d added a few virtual destructors to prevent memory leaks. TimQu 2017-04-19 15:23:56 +0200
  • 8c6b22bebc Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests TimQu 2017-04-13 09:37:54 +0200
  • 38eadad17d Jit: Expression labels which occur twice in list of formulae now supported Sebastian Junges 2017-04-19 13:46:44 +0200
  • a21995052c fix for probabilistic reachability formulae Sebastian Junges 2017-04-19 13:44:47 +0200
  • 7170fea7ce Jit Fix for LTS support Sebastian Junges 2017-04-19 11:28:46 +0200
  • 1a37ef8fd2 Merge branch 'master' into refactor_pla TimQu 2017-04-19 11:37:07 +0200
  • 1a9589dfa6 Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests TimQu 2017-04-13 09:37:54 +0200
  • 81ecf752c8 better diagnostic for unsupported model type in JIT builder dehnert 2017-04-19 10:54:04 +0200
  • 86a783de92 two more fixes for issues pointed out by Tim: concurrency bug in sylvan and bug in symbolic quantitative check result dehnert 2017-04-14 11:43:07 +0200
  • ec10072341 Merge branch 'master' into simplified_levels sjunges 2017-04-18 21:06:05 +0200
  • 970b72786c disable level simplification for now sjunges 2017-04-18 20:00:21 +0200
  • 7aa6215ed3 Got rid of an outdated error message for reused actions in JitBuilder Sebastian Junges 2017-04-18 19:46:55 +0200
  • 1b79bcc169 DdJani now builds LTS as an MDP. Sebastian Junges 2017-04-18 19:46:25 +0200
  • 4c99790213 Minor updates to ExprTk ArashPartow 2017-04-13 08:35:42 +1000
  • 977dd1ef53 Get GMP location from carl, set it as a hint for sylvan. sjunges 2017-04-12 21:59:12 +0200
  • a371301312 We require gmp, so we can as well just set the corresponding flag to true. sjunges 2017-04-12 21:58:42 +0200
  • 1c22fdabe1 Edit in Sylvan/cmake: Allow for hints about gmp location sjunges 2017-04-12 21:58:06 +0200
  • 97a7689c67 gcc and clang working on Debian Stretch again dehnert 2017-04-11 20:21:47 +0200
  • 6d9e906291 remove LTO from sylvan as it causes more problems than it solves dehnert 2017-04-11 10:58:34 +0200
  • ec3468aef5 hopefully fixed the compile issue on Linux dehnert 2017-04-10 21:52:32 +0200
  • 4e1855a440 use of intermediate value to make conversion work with gmp dehnert 2017-04-10 09:22:59 +0200
  • bae4b421ab added missing template instantiation and print more info on LTO in cmake dehnert 2017-04-07 15:37:21 +0200
  • 8bfa699519 attempt to fix link error sjunges 2017-04-06 23:30:17 +0200
  • cd954aacd9 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm sjunges 2017-04-12 22:00:08 +0200
  • 233c063ad8 statistics output for multi-obj model checking when -stats option is given TimQu 2017-04-12 18:49:37 +0200
  • 2e01c8b137 Fixed time bounds containing constant variables for multi objective formulas. TimQu 2017-04-12 16:45:08 +0200
  • 6598c2707c Merge remote-tracking branch 'origin/master' into refactor_pla TimQu 2017-04-12 09:14:20 +0200
  • 9f795ffccd Merge branch 'master' into refactor_pla TimQu 2017-04-12 09:14:13 +0200
  • 187e8bc52b fixed two bugs related to hybrid quantitative results dehnert 2017-04-11 22:19:15 +0200
  • a896c0df28 improved exact computations TimQu 2017-04-10 15:08:27 +0200
  • 09552d43a3 IsExact number trait TimQu 2017-04-10 15:03:28 +0200
  • ee754c96e2 renamed ParameterLifting.h -> RegionChecker.h TimQu 2017-04-10 13:42:12 +0200
  • ab7b31b08c optimized memory requirements when a large amount of regions is to be analyzed. Also: Progress bar :) TimQu 2017-04-10 13:10:50 +0200
  • 2647ffa9ae added test for exact validations TimQu 2017-04-10 11:29:25 +0200
  • d659d193bc Fixed game solver test and potential memory leaks TimQu 2017-04-10 11:29:05 +0200
  • 2cdda140b8 Minor updates to ExprTk ArashPartow 2017-04-10 19:01:40 +1000
  • de87ff1152 fixed finding of z3 library when its location is given via -DZ3_ROOT TimQu 2017-04-07 17:27:45 +0200
  • f59e9a7f77 added flushing of cout in STORM_PRINT macro TimQu 2017-04-07 17:13:47 +0200
  • 367b8f0a3e parameter lifting with hybrid engine TimQu 2017-04-07 17:07:26 +0200
  • bb3c2bd556 Implemented policy iteration for game solver TimQu 2017-04-07 15:19:58 +0200
  • 0d9205c0e6 Fixed case in include path Matthias Volk 2017-04-07 10:52:09 +0200
  • 00c210565b Merge from dft_case_study Matthias Volk 2017-04-07 10:24:42 +0200
  • e05672a87d Merge branch 'master' into refactor_pla TimQu 2017-04-07 00:09:06 +0200
  • 936293e318 Refactored GameSolver. It is now analogous to the MinMaxLinearEquationSolver. TimQu 2017-04-06 23:56:48 +0200
  • 77e71b7876 capitalization error and fix for cumulative rewards TimQu 2017-04-06 23:05:31 +0200
  • c16390e7f5 Equality Comparisons for JaniVars, just to make life easier :-) sjunges 2017-02-08 22:57:20 +0100
  • 3eb675f8c0 used helper methods instead of own implementations TimQu 2017-04-06 15:57:30 +0200
  • 502cf4d6e0 extended model checker hint functionality to bypass the maybestates computations TimQu 2017-04-06 15:12:56 +0200
  • becc43e1e1 added wokaround proposed by jklein to make the new sylvan version build on older osx dehnert 2017-04-05 17:26:01 +0200