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

Commit Graph

  • 9c0b5b028c Finding z3 in system, cleaned some cmakelists. sjunges 2015-08-03 18:14:13 +0200
  • f879c608eb fix for wrong ifdef dehnert 2015-08-03 16:25:09 +0200
  • ecb37ccd1d made compilation of ConstraintCollector in Dtmc predicated on CARL being available dehnert 2015-08-03 16:09:49 +0200
  • d62539165e 'Identity updates' can now be described as applying 'true' in PRISM programs. dehnert 2015-08-03 15:36:45 +0200
  • ec74d01557 Fix in the comment. sjunges 2015-08-03 14:04:23 +0200
  • f2c6bb91fd Some extra methods for the Expr. Manager. sjunges 2015-08-03 14:03:03 +0200
  • d8a3009bde merged master in future branch sjunges 2015-07-31 10:48:14 +0200
  • 57987c1387 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-07-31 10:40:13 +0200
  • 5fddb47a91 some cleaning and extra comments in the CMakeLists sjunges 2015-07-31 10:39:13 +0200
  • 1ec453e587 support for intervals in matrices sjunges 2015-07-30 18:13:02 +0200
  • 0c2ada4627 Merge branch 'global_variables' into future sjunges 2015-07-30 18:11:12 +0200
  • 8b1e003657 Fix sjunges 2015-07-29 12:08:01 +0200
  • 9a0e42babb static analysis for global variables sjunges 2015-07-28 19:07:52 +0200
  • 7a050434d9 bugfixes for NondeterministicModel, improvements for StateActionPair, graph and initialize sjunges 2015-07-27 17:22:22 +0200
  • 7b2bfa592c started working on integration of games-based abstraction refinement in production code quality dehnert 2015-07-24 17:37:51 -0700
  • a212cce8c1 Added a method to get the number of choices for a specific state. sjunges 2015-07-24 12:22:39 +0200
  • b50c823c77 Refactored for faster compilation times. sjunges 2015-07-24 12:12:28 +0200
  • cf8da8a8df wrappers for common tuples added sjunges 2015-07-24 11:58:35 +0200
  • 9d5c3e7e2f added functionality to flatten the modules of a PRISM program into one module dehnert 2015-07-23 23:23:35 -0700
  • 4dbbe3c561 moved constraint collection to DTMC class dehnert 2015-07-23 11:12:21 -0700
  • 86ff07ec0d take sampling point before approximation to know whether to minimize or maximize. only compute the rational function when it is needed. TimQu 2015-07-21 09:32:36 +0200
  • 37eacf574b Further work on state space generation sjunges 2015-07-20 17:57:42 +0200
  • 27b87c6d78 Merge branch 'master' into TimParamSysAndSMT TimQu 2015-07-19 17:01:26 +0200
  • a22c36e38a avoided unnecessary copy of matrix while doing graph analysis. const& was missing somehow. TimQu 2015-07-19 16:56:12 +0200
  • 777942f5d3 renamed BoundType to CoefficientType, better region.getVariables TimQu 2015-07-19 16:31:08 +0200
  • 904126fcab Merge branch 'master' into TimParamSysAndSMT TimQu 2015-07-19 16:27:47 +0200
  • 59fe9ace09 Further work on state space generation sjunges 2015-07-17 14:06:15 +0200
  • 63618147b8 - Compute sample points via instantiated DTMCs - Use the same mdp for the different regions and just change the entries of the matrix accordingly TimQu 2015-07-11 21:23:48 +0200
  • fd3ffafcd9 First version of the monolithic state space generation sjunges 2015-07-08 15:47:51 +0200
  • fcdf0eee7a changes on the solver interface to work with timeouts or memouts. i.e. there is no exception thrown in that case TimQu 2015-07-06 22:29:02 +0200
  • 076b6cc71c reimplemented region model check via smt solving TimQu 2015-07-05 19:38:28 +0200
  • c99a61307f hybrid dtmc model checker can now also treat lra dehnert 2015-06-22 17:05:30 +0200
  • 39abecbad3 added some tests for LRA in CTMCs dehnert 2015-06-22 14:33:29 +0200
  • 13514c9da8 hybrid CTMC model checker can now do lra as well dehnert 2015-06-21 22:58:44 +0200
  • 1e5398c8b7 LRA finally working for ctmcs dehnert 2015-06-20 20:07:45 +0200
  • 331ea9fc19 further work on steady state probabilities dehnert 2015-06-19 16:56:47 +0200
  • b9cc6c2708 fixed bug in concatenating results of subformulas dehnert 2015-06-18 22:15:00 +0200
  • a412ac2a60 Progress in smtrat-smtsolver interface sjunges 2015-06-18 22:14:52 +0200
  • 40a0f4f18a stupid fix in cli (carl version can not be shown, no idea how...) sjunges 2015-06-18 22:14:12 +0200
  • 7cbab6a260 use gmpxx mpq_class for rational numbers sjunges 2015-06-18 19:50:54 +0200
  • 1b9860ece0 modified parser to accept more legal formulas dehnert 2015-06-18 19:35:52 +0200
  • 16c57decff print header including info for smtrat and carl (untested) sjunges 2015-06-18 19:33:50 +0200
  • 50136dd31a Improved import of carl/smtrat sjunges 2015-06-18 17:27:50 +0200
  • 71f8504c08 included a necessary header which was indirectly included before to ease further implementations of the smtsolver interface sjunges 2015-06-18 17:01:29 +0200
  • ce58a5fa6f steady state working for CTMCs dehnert 2015-06-18 13:40:16 +0200
  • fab39f1ac2 Finding smtrat via their new export version Sebastian Junges 2015-06-18 13:12:11 +0200
  • d3124f2c23 fixed bug in matrix builder dehnert 2015-06-17 22:36:47 +0200
  • 6c4162fae4 more work towards steady state for CTMCs dehnert 2015-06-17 21:38:46 +0200
  • 1130efe0dc step towards steady-state for CTMCs dehnert 2015-06-17 18:11:41 +0200
  • 4c35bc0f66 symbolic DTMC model checker working dehnert 2015-06-17 16:53:34 +0200
  • 81c627b9b7 First version of fully symbolic game solver. dehnert 2015-06-11 20:45:52 +0200
  • 96464fdcbc added model classes for two-player stochastic games dehnert 2015-06-11 17:21:32 +0200
  • 37cd2ad682 started working on game solver dehnert 2015-06-10 16:22:29 +0200
  • c9c6d1e199 Implemented mdp building and checking TimQu 2015-06-07 21:00:44 +0200
  • 3bb0346407 Fixed missing typenames and member initialization reordering. PBerger 2015-06-04 15:24:49 +0200
  • 0c3c057f83 Fixed the usual "typename" errors in Clang-code. PBerger 2015-05-30 18:16:35 +0200
  • dce1d728e5 I added a few small documentation fixes. PBerger 2015-05-30 17:42:15 +0200
  • b9eaddfcb3 Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2015-05-30 17:28:34 +0200
  • 772ab33ad1 Merge remote-tracking branch 'remotes/origin/master' David_Korzeniewski 2015-05-30 17:22:18 +0200
  • 5623e66566 Ignore empty lines in property file and only warn if a line could not be parsed David_Korzeniewski 2015-05-30 17:21:28 +0200
  • a4663ccfd3 added missing input file for tests dehnert 2015-05-30 17:06:13 +0200
  • 68b786d47b Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-05-30 16:58:01 +0200
  • f672f8d8d8 Merge branch 'mtbddIntegration' dehnert 2015-05-30 16:57:47 +0200
  • 21d1039152 Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2015-05-30 16:47:35 +0200
  • c3d0112975 Actually try to read all lines from property file David_Korzeniewski 2015-05-30 16:34:37 +0200
  • 287393abc4 Added Policy Iteration to the NativeMinMaxLinearEquationSolver. Added a test. PBerger 2015-05-30 16:06:00 +0200
  • 56e1b79085 Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2015-05-29 22:24:23 +0200
  • f63e5fc873 Implemented Policy Iteration inside the GmmxxMinMaxLinearEquationSolver. Added an option for selecting Value- or Policy Iteration in the GeneralSettings. PBerger 2015-05-29 22:24:06 +0200
  • 7d84b0a4c5 Added ability to check properties from property file to cli utility. Added minimal example for lra on dtmc David_Korzeniewski 2015-05-29 16:41:25 +0200
  • 6206147e1a Sampling the corners of the region TimQu 2015-05-27 21:33:22 +0200
  • 47f2e9592b Implemented preprocessing steps TimQu 2015-05-25 22:42:56 +0200
  • 1c0438ff38 a few steps to efficiently analyze multiple regions... TimQu 2015-05-25 14:06:29 +0200
  • ccfb452f53 no hardcoded regions anymore TimQu 2015-05-23 20:34:28 +0200
  • 836b5cebc6 implemented some auxilarry functions for parameterregions TimQu 2015-05-13 22:04:33 +0200
  • 1cf0a73c4e Added methods to update nonzero entry count and update it when necessary David_Korzeniewski 2015-05-07 18:18:26 +0200
  • cf5442fe45 Bugfix and test-fix: Only the "never leave MEC"-states have cost > 0 and transition costs are all 0 in the ssp. David_Korzeniewski 2015-05-07 16:23:29 +0200
  • 8e688f71ff Tests for DTMC LRA and some bugfixes. All tests pass. David_Korzeniewski 2015-05-07 13:07:40 +0200
  • 5acaed6048 Added flag to keep zeros when transposing. David_Korzeniewski 2015-05-07 13:07:00 +0200
  • 0ba629ad3f More tests, bugfixes: All tests pass. David_Korzeniewski 2015-05-06 23:06:01 +0200
  • dfab1c291c Error fixed. David_Korzeniewski 2015-05-06 23:05:38 +0200
  • 716cf3abdd Adapted to new solver interface some tests and bugfixes. Tests still failing. David_Korzeniewski 2015-05-04 23:35:35 +0200
  • 3872e17a4e Merge branch 'master' into LRA_for_dtmc_mdp David_Korzeniewski 2015-05-04 21:42:35 +0200
  • f6c4b9be72 splitted "elimination model checker" and "region model checker" into two files. TimQu 2015-05-03 18:25:20 +0200
  • 96cf3c65bb implemented instantiation as mdp to get valid bounds TimQu 2015-05-03 15:31:54 +0200
  • d4f051c4f0 Fixed Windows build David_Korzeniewski 2015-05-01 14:46:26 +0200
  • 073ce2ee2c Merge branch 'master' into LRA_for_dtmc_mdp David_Korzeniewski 2015-04-29 20:46:53 +0200
  • 1f87e7c8b2 First test for LRA on MDPs David_Korzeniewski 2015-04-29 20:35:16 +0200
  • 8fc58439bc Computing LRA as expected reward in MDPs. David_Korzeniewski 2015-04-28 19:56:02 +0200
  • 4ab84bc42c state elimination -- hybrid and standard method TimQu 2015-04-25 18:44:10 +0200
  • e4968b1dde Fixed minor issue in cli dehnert 2015-04-24 08:59:34 +0200
  • 0e1552d3a5 eliminating of states with constant outgoing transitions TimQu 2015-04-22 21:49:35 +0200
  • d9613b20c8 restriction of the state probability variables TimQu 2015-04-21 21:29:00 +0200
  • 0fdb3685d1 Computing LRA for states not in bsccs as expected reward David_Korzeniewski 2015-04-17 18:02:41 +0200
  • 916c821b3e Compute steady state for all BSCCs together by solving just one equation system instead of solving an equation system for each BSCC. David_Korzeniewski 2015-04-17 16:55:12 +0200
  • bac0e01835 added time measurement, support for stateelimination TimQu 2015-04-14 21:29:08 +0200
  • dd399c5f85 Finalized hybrid MDP model checker. It passes its tests now. dehnert 2015-04-11 17:55:45 +0200
  • 2b807dd72e implemented communication with solver TimQu 2015-04-11 17:09:17 +0200
  • 2bf7eafb4b Further work on hybrid MDP model checker. dehnert 2015-04-10 20:37:57 +0200
  • 9a83dfac10 Typo in DTMC, tried to use same approach for MDPs, which won't work. David_Korzeniewski 2015-04-10 18:33:26 +0200
  • e3320ee086 Started working on hybrid MDP model checker. dehnert 2015-04-10 17:57:24 +0200