Commit Graph

Select branches

Hide Pull Requests

main

tempestpy_adaptions

Mono Color

• eeb7a21cf9 Merge branch 'reduceCompiletime' masawei 2013-11-30 14:55:16 +0100
• 281140c8ff Sketched algorith outline for time-bounded reachability for Markov automata. dehnert 2013-11-29 15:42:05 +0100
• dabfb5e1dd First working version of LRA computation for Markov automata. dehnert 2013-11-27 16:07:39 +0100
• 339b598694 Enabled computation of LRA for individual maximal end components. It remains to compute the overall LRA value using the values for the individual MECs. dehnert 2013-11-26 21:36:41 +0100
• 45f137face Prepared stub for Long-Run Average computation for Markov automata. dehnert 2013-11-26 17:08:41 +0100
• 775382fa91 Added option to encode reachability of a target state for SAT-based minimal command counterexample generation. Fixed bug in vector-based set. dehnert 2013-11-26 11:11:53 +0100
• ad0bba6223 Started work on including reachability encoding in SAT-based counterexample generator. dehnert 2013-11-25 18:29:02 +0100
• ea7f48cff6 Introduced solver header in utility to return standard solvers when requested. dehnert 2013-11-25 17:22:00 +0100
• a229b9b322 Refactored MILP-based command generator to use a general LpSolver interface, so other LP solvers may be used when needed. dehnert 2013-11-25 13:16:39 +0100
• 9f7a0f1354 Started abstracting LP solvers into a common interface. This way, we have more freedom to target different LP solvers easily and can avoid licensing problems. dehnert 2013-11-24 21:54:40 +0100
• 101c39f365 Added correct detection of states that possess infinite exptected time to reach a given goal set. dehnert 2013-11-22 18:22:58 +0100
• daea775263 Now rates get correctly transformed to probabilities + exit rates for Markov automata. dehnert 2013-11-21 19:22:51 +0100
• f1a9b1e602 First version of minimum expected time for Markov automata. dehnert 2013-11-21 17:15:22 +0100
• 2cbdf56267 Fixed some bugs in bit vector and vector set that prevented the MEC decomposition from functioning correctly. dehnert 2013-11-20 12:45:31 +0100
• bfb416687f Bugfix for Markov automaton parser. Number of choices now gets computed correctly in the presence of deadlock states. dehnert 2013-11-19 22:33:51 +0100
• e885603d92 Added new Markov automaton example. dehnert 2013-11-19 18:14:49 +0100
• f35ac73547 Splitted VectorSet in header/source file which caused certain minor changes in its interface. Fixed some issues in the Markov automaton parser and made it substantially faster by dropping sscanf. This however introduces other limitations that need to be addressed in the future. dehnert 2013-11-19 16:54:24 +0100
• 5a9d778a23 First version of MEC decomposition for nondeterministic models. dehnert 2013-11-19 14:02:15 +0100
• b9130180ee Rough sketch of MEC decomposition. dehnert 2013-11-18 22:35:45 +0100
• f287b7e760 Further steps towards implementation of MEC decomposition. dehnert 2013-11-18 17:21:29 +0100
• 84f6bf7104 Added a getBackwardsTransitions() to AbstractNondeterministicModel, since simple transposition does not yield correct results and for the computation of the backwards transitions the nondeterministic choice indices must be known. |-> Ran the tests: all green. masawei 2013-11-26 23:01:50 +0100
• bd367f89c7 Enabled model checking of PCTL properties for symbolic models. dehnert 2013-11-26 21:34:46 +0100
• 170306e46d Moved SparseMatrix transposition function from AbstractModel (named: getBackwardsTransitions) to SparseMatrix (named: transpose) where it belongs. - Fixed one problem marked FIXME in the transpose function. The need for a "sentinel" element was created by an off by one in the prior loop. - Changed all occurences of SparseMatrix<bool> to SparseMatrix<T>. Now the only two types for which SparseMatrix is instantiated are double and int. - Compiles again. |-> Compile time seems to be roughly the same for clean; make all. For incremental builds I haven't tested yet. masawei 2013-11-25 21:15:36 +0100
• c30d6d307e Figured out how to explicitly instantiate templates. But got bitten by std::vector<bool> as it is specialized and uses bitsets (i.e. integers) internally. Less memory but at the cost of 'oh, sorry std::vector<bool> does not return a bool&'. That again seems to be a problem for the SparseMatrix<bool> instatiation since for instance getValue returns a T&. On the one hand I don't quite know why this was never an issue before and on the other hand it prevents successful compilation. So there are different ways to settle this: - Specialize SparseMatix for bool -> possibly lots of code, but might be the best solution - Write a wrapper for std::vector that uses chars instead of booleans - Dont't use SparseMatrix<bool> masawei 2013-11-18 23:27:45 +0100
• eca717759a Added functionality to apply a scheduler to a Markov automaton. dehnert 2013-11-17 18:48:16 +0100
• c5ff387b98 Merge branch 'master' into imca dehnert 2013-11-17 18:31:00 +0100
• e31c3bfb17 Added an important comment. dehnert 2013-11-17 18:29:13 +0100
• 360b506afe Sparse MDP model checker now correctly computes (memoryless) schedulers for Until and Reachability Reward formulas. dehnert 2013-11-17 18:24:44 +0100
• 9e941e6b4a Added scheduler classes. Added method to model classes that applies a scheduler. dehnert 2013-11-17 17:20:18 +0100
• 09f192b40f Refactored SCC-Decomposition design as a preparation step for computing maximal end components of Markov automata. dehnert 2013-11-17 15:29:09 +0100
• 1c594d02f5 Added check in Markov automaton parser to ensure the Markovian choice is the first one for each state. This way only the Markovian states need to be stored and by convention their first choice is the Markovian one. dehnert 2013-11-16 00:07:11 +0100
• 66f15efbc6 Fixed memory bug in Markov automaton parser. dehnert 2013-11-15 23:28:51 +0100
• d725a3f898 Removed bit vector for storing markovian choices of MA. From now on, the first choice of a hybrid/Markovian state is the Markovian one. dehnert 2013-11-15 12:53:26 +0100
• 9e66447eb2 Add "lib" prefix for z3 only on Windows David_Korzeniewski 2013-11-15 12:21:05 +0100
• cebda374d1 Further step towards Markov automata parser. dehnert 2013-11-14 21:25:21 +0100
• c02f4e2adc Markov Automata transitions can now be parsed. Next up: a parser that combines transition and label parsing for Markov automata. dehnert 2013-11-14 16:17:46 +0100
• 873373eb4e Further work on explicit MarkovAutomaton parser. dehnert 2013-11-14 15:18:15 +0100
• 77cabe1948 Started implementing a parser for an explicit format for Markov automata. This commit breaks things, so don't pull if you want to have a running version of this branch. dehnert 2013-11-13 22:04:40 +0100
• 4fcd4c5961 Merge remote-tracking branch 'remotes/origin/master' David_Korzeniewski 2013-11-13 20:39:39 +0100
• 7c0dd5eaf5 Fixed build errors on Windows David_Korzeniewski 2013-11-13 20:38:11 +0100
• bc94f69c0b Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux. dehnert 2013-11-13 15:07:20 +0100
• 4550422fac Added formula support for PRISM models. ExplicitModelAdapter now properly checks for out-of-bound values for integer variables. dehnert 2013-11-08 00:06:21 +0100
• 5cd18c1cf5 Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux. dehnert 2013-11-13 15:07:20 +0100
• d43318afd8 Added first version of MarkovAutomaton class. dehnert 2013-11-13 14:05:48 +0100
• 78d5f89ea2 Added formula support for PRISM models. ExplicitModelAdapter now properly checks for out-of-bound values for integer variables. dehnert 2013-11-08 00:06:21 +0100
• 141fdca6d7 Added initial version of MarkovAutomaton class. dehnert 2013-11-07 16:15:48 +0100
• 4cdf1e6b7a Fixed warning resulting from wrong initialization order. dehnert 2013-11-07 13:37:25 +0100
• 94d8a46b1d Fixed some compile errors originating from the introductionof the new storm::storage::VectorSet. - Also handled the case of a missing --prctl while using the counterexample generation. - Remark: Some documentation for the VectorSet would have been nice. masawei 2013-11-05 22:20:15 +0100
• afb0b19c27 All merge conflicts resolved. Also one small change I forgot before the merge: - The counterexample generation again uses the --prctl option to aquire its formulas. masawei 2013-11-05 21:41:57 +0100
• 8ed3759074 Merge branch 'critSubsysMerge' masawei 2013-11-05 21:39:57 +0100
• af0601c453 Made several changes. - Fixed the infinite loop bug that occured when giving a filepath pointing to a directory instead of a file. - The BitVector to Dtmc subsystem converter now supports an optional choice labeling. - The output of the modelchecker to the log file is now suppressed while doing a counterexample generation. - It is now possible to add more atomic propositions to the AtomicPropositionLabeling than previously declared (at the cost of one reserve per added ap beyond the maximum). The maximum is then increased accordingly. |-> As a result the state added for the Dtmc subsystem has now its own label. masawei 2013-11-05 00:56:44 +0100
• e3e02ecce2 Made counterexample generation output usable. -std::cout gives enough information to understand what th result of the generaton is. -Added another argument to --counterExample specifying a directory to write .dot files containing the critical subsystems (as Dtmc) to. -Cleaned up some logging output of the counterexample generationn. masawei 2013-10-28 23:04:14 +0100
• 393a72d56f Added handling of state and transition rewards to getSubDtmc(). Remark: I don't quite get the optional choice labeling in Dtmcs. Whats its purpose? Why is it undocumented in the Dtmc constructor, not supported by the parser but needed nevertheless? masawei 2013-10-28 18:29:40 +0100
• ee1c1eb9b6 First implementation of the BitVector to Dtmc subsystem converter in Dtmc.h -Had to add a addState function to AtomicPropositionLabeling to be able to throw out the unneeded states using the substates constructor while at the end adding the absorbing state and its label. An alternative for that would be to provide a constructor taking the mapping and the single labelings vector as well as a getter for the single labelings. -The --counterexample command now only uses the pctl file given as argument to it and therefore it is now superflous to give the --prctl command in that case. -Also fixed a bug in the filter constructor of the BitVector. Now it copies all bit values specified by the filter to the correct index of new instance instead of all to index 0. masawei 2013-10-28 01:39:20 +0100
• 13d66a504f (Hopefully) Finally made cuts correct. Luckily, this even improves performance on some models. dehnert 2013-10-27 22:00:08 +0100
• a98310a723 Some code revisions. masawei 2013-10-26 17:02:27 +0200
• a33717787c Bugfixes for new set class. dehnert 2013-10-24 16:28:37 +0200
• 62b4eb1cde Minor bugfixes. dehnert 2013-10-24 00:04:56 +0200
• 422da8f481 Added set class with an underlying vector container. Adapted code in counterexample generators to use the new set class. Still bugs in it though. dehnert 2013-10-23 17:09:39 +0200
• 58fa1a46a0 Added some comments. dehnert 2013-10-22 23:08:40 +0200
• e0fbb5cbea Added proper treatment for both upper bound operators to counterexample generators. Added optional statistics output to SAT-based counterexample generator. dehnert 2013-10-22 16:06:53 +0200
• 82f970356e Introduced analysis for labels that could potentially improve a solution. dehnert 2013-10-21 20:32:50 +0200
• 0329899304 Removed debug output from Z3 adapter. Put new backward cuts in actions. dehnert 2013-10-21 18:36:48 +0200
• e24c64e41e Refinement work on backward implications. dehnert 2013-10-21 17:28:56 +0200
• 2201581ac3 Further improved treatment of solutions with only unreachable target states. dehnert 2013-10-20 23:07:55 +0200
• dc0be79172 Improved elimination of solutions in which the target states are not even reachable. dehnert 2013-10-20 21:17:26 +0200
• b74715a374 Force Gurobi to be more precise wrt. binary variables. dehnert 2013-10-20 11:58:58 +0200
• 1b2bb9c138 Set up command flow for subsystem generation. Results seem correct on the first look. masawei 2013-10-19 21:51:11 +0200
• 9143e09d86 Added some more output to counterexample generators for benchmarks. dehnert 2013-10-19 19:08:33 +0200
• d3dee7dd3e Minor changes to counterexample generator settings and output. dehnert 2013-10-18 09:08:26 +0200
• 5adb9e2f6b Renamed option file for counterexample features. dehnert 2013-10-17 22:23:53 +0200
• e97680d37d Added counterexample property files for some models. dehnert 2013-10-17 22:20:17 +0200
• 47a05fc1b0 Beautified output of option system. Enabled command line interface of counterexample generation. dehnert 2013-10-17 22:19:24 +0200
• e2d4a5c1d3 Started work on beautifying Option-System output. dehnert 2013-10-17 14:36:47 +0200
• b61090fe92 Merge branch 'master' into MinimalCommandCounterexample dehnert 2013-10-17 09:12:38 +0200
• b18199d3ec Further work on minimal label set generators. dehnert 2013-10-16 21:04:05 +0200
• ad7f800ac0 Added examples from MILP-paper. dehnert 2013-10-16 11:13:22 +0200
• c31dbc85a7 Made all examples from the MILP-paper work. Most of them are really slow though. dehnert 2013-10-16 11:11:24 +0200
• b55932b212 Adapted subsystem generation to the use of the new subsystem checking method using bit vectors. Compiles now. Next up: Setting up the control flow to make it actually generate a critical subsystem. masawei 2013-10-16 01:28:27 +0200
• 4dca7abd3f Implementaed methods for checking until formula by providing the left and right states instead of the whole formula (same with bounded Until) in the SparseDtmcPrctlModelChecker, analouge to the SparseMdpPrctlModelChecker. Reverted unnecessary changes to the AbstractModel checker. Next on the list: Adapting the subsystem generation routine to the new method of providing the subsystem to the model checker. masawei 2013-10-16 00:01:33 +0200
• 86909937f3 Grammar now supports min/max/floor/ceil functions. Parsing still has errors though. dehnert 2013-10-15 22:29:28 +0200
• e8b83a6aab Added synchronization cuts. dehnert 2013-10-15 20:47:41 +0200
• 641c09dcfa Fixed compile errors on windows caused by missing includes and use of initializer lists (not supported by vs11) David_Korzeniewski 2013-10-15 20:44:08 +0200
• e8f1c7c9ab Fix to grammar to allow for empty probability in updates. dehnert 2013-10-15 15:09:19 +0200
• 0cb390b186 More integration work. Ran into problem with the AbstractModelChecker being declared const for the model check. I use it for the subsystem generation and tell it what the current subsystem is. so I have two options: 1. Carry the subsystem as argument through all checking functions of the complete checking tree 2. Store the subsystem in the checker and use it in checkAp to induce the correct result back through the tree. In the original implementation I used option 2. But that does only work if it is not constant. masawei 2013-10-14 11:53:49 +0200
• 6a4d2183dc Fix for SAT-based minimal counterexample generator: backward cuts are now fully correct again. Fix for PRISM grammar: missing update probabilities now default to one. dehnert 2013-10-14 11:19:26 +0200
• 8244420248 Some refactoring work. dehnert 2013-10-13 20:49:03 +0200
• 4d161e5e8e Began with integration of crit. subsystem generation into master. Still some compile errors to fix. masawei 2013-10-12 22:21:20 +0200
• 1716c45ec5 Fixed compile errors concerning the handling of the STORM_HAVE_Z3 flag and a missing include in IRUtility.h Should now compile again. masawei 2013-10-11 16:01:29 +0200
• ae6838d786 Switched to different computation of smallest model. dehnert 2013-10-11 15:20:45 +0200
• 54d28e5540 Further work on MaxSAT-based minimal command set generator. dehnert 2013-10-11 09:49:28 +0200
• fda9c43e86 Fix for SMT-based minimal command set generator. Minor fixes to string output of expression classes. dehnert 2013-10-10 17:22:35 +0200
• a2bba28f94 Moved static analysis for guaranteed label set computation into utilities and improved MILP-based approach by using this information. dehnert 2013-10-09 22:36:41 +0200
• 629448c312 First working version of MaxSAT-based minimal command counterexample generation. dehnert 2013-10-09 16:46:28 +0200
• b6ff62e689 Towards adding more cuts to MaxSAT-based minimal command counterexamples. Some fixes here and there along the way. dehnert 2013-10-08 22:11:41 +0200
• d6c59e2ca3 Further work on MaxSAT-based minimal counterexample generator. dehnert 2013-10-08 16:23:39 +0200
• b860f16ada Further work on MaxSAT-based minimal command counterexamples. dehnert 2013-10-07 22:02:22 +0200
• aec2596753 Several fixes for the IR. Weakest precondition computation is now supported for IR expressions. dehnert 2013-10-07 16:14:00 +0200
• f7a578e65d Major change in PRISM grammars and IR: the IR now uses unique pointers instead of shared pointers to express ownership of objects more clearly. dehnert 2013-10-07 11:55:59 +0200
• 20ae92e1ba Added support for cloning IR expressions. dehnert 2013-10-05 20:46:37 +0200