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

Commit Graph

  • 628219298e Some small cleanup in verification API Matthias Volk 2019-08-05 16:37:43 +0200
  • d39189c0e2 Scheduler extraction for MA properties which can be reduced to MDP queries Matthias Volk 2019-08-05 13:16:16 +0200
  • cdaea9ea55 Small fix in DRNParser Matthias Volk 2019-08-02 21:00:27 +0200
  • 39cedc223e Use ValueParsen in DFTJsonParser Matthias Volk 2019-08-02 20:59:56 +0200
  • fba3223f63 Use typedefs of RationalFunctionAdapter Matthias Volk 2019-08-02 20:33:54 +0200
  • 30565e4d0c Use carl hashing functions Matthias Volk 2019-08-02 19:03:28 +0200
  • 2433671b7d Changelog update Tim Quatmann 2019-08-01 16:28:26 +0200
  • d4ee19c350 Merge branch 'lra-strategies' Tim Quatmann 2019-08-01 16:17:27 +0200
  • 42b7865e7e DirectEncodingParser: Added support for Action-based rewards. Tim Quatmann 2019-08-01 16:14:26 +0200
  • 429c91ff13 Added support for parsing fractions in DRN files. Tim Quatmann 2019-08-01 15:27:34 +0200
  • b896726c4a Include choice labels in exported scheduler. Tim Quatmann 2019-07-31 19:03:20 +0200
  • a47945a931 Cleaner output when exporting schedulers Tim Quatmann 2019-07-31 19:03:02 +0200
  • 8a23197a77 Fix for LRA scheduler generation. Tim Quatmann 2019-07-31 19:02:36 +0200
  • 72425ec1b2 CLI: Added an option to export the produced scheduler to a file. Tim Quatmann 2019-07-31 18:45:01 +0200
  • 009cee1c25 Implemented scheduler extraction for LRA properties for MDP. Tim Quatmann 2019-07-31 18:44:18 +0200
  • badd645026 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-30 17:21:24 +0200
  • c1b3a4f991 LraMdpPrctlModelCheckerTest: Test LRA computation for different environments. Added a testcase. Tim Quatmann 2019-07-30 17:19:13 +0200
  • 622926d9c1 LpChecker: Added a redundant constraint, improved stability. Tim Quatmann 2019-07-30 16:44:36 +0200
  • 63fe1c01d1 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-30 08:54:07 +0200
  • 48dbaa6fbd Fixed a test Tim Quatmann 2019-07-30 08:52:51 +0200
  • 16aee7c386 fixed a typo Tim Quatmann 2019-07-30 08:52:15 +0200
  • 9e63a89db7 Fixed operator precedence for power and modulo operator thanks to help from Joachim Klein. Matthias Volk 2019-07-29 20:55:20 +0200
  • d05b132dde Better error output Matthias Volk 2019-07-29 20:55:13 +0200
  • 4578e06555 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-29 16:56:26 +0200
  • 900da9e556 Fixed EndComponentEliminatorTest Tim Quatmann 2019-07-29 16:56:19 +0200
  • aabb63846a Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-29 16:31:21 +0200
  • 2cb7b5769e Jit: Fixed issues when CLN and/or GMP is installed via carl Tim Quatmann 2019-07-29 16:31:12 +0200
  • f83c0fa606 MultiObjectivePreprocesso: Fix for new preprocessing in case of multi-dimensional bounded until formulas. Tim Quatmann 2019-07-29 16:29:01 +0200
  • 9e510560c9 MultiobjectivePreprocessor: Fixed removal of irrelevant states. Tim Quatmann 2019-07-29 10:57:04 +0200
  • 9526720a9c Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-26 14:50:30 +0200
  • b1b429e8d2 EndComponentEliminatorTest: Made the test more stable with respect to different orders in the result. Tim Quatmann 2019-07-26 14:42:14 +0200
  • 925f72f754 More testcases for multi-objective model checking with scheduler restrictions (including fixes). Tim Quatmann 2019-07-26 14:37:42 +0200
  • b308f4e1d0 Initialize region before creating sample points Jip Spel 2019-07-26 11:47:40 +0200
  • 12e0ef537c Small fixes Jip Spel 2019-07-26 11:12:00 +0200
  • 1f68e1d05e Multi-objectivePreprocessor: identify a subset of the states that can be made absorbing. Tim Quatmann 2019-07-26 08:46:32 +0200
  • 92dd97b06a Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-26 08:45:28 +0200
  • 492348542f SubsystemBuilder: Fix deadlocks with a selfloop (if requested) Tim Quatmann 2019-07-26 08:44:55 +0200
  • 0b1b0d97e2 utility/graph: fixed behavior of getReachableStates when an initial state is not in the constrained set. Tim Quatmann 2019-07-26 08:42:39 +0200
  • 3e8f53f640 Added test cases for multi-objective scheduler restriction checker. Tim Quatmann 2019-07-26 08:40:12 +0200
  • 2aa385905b DetSchedsLpChecker: Switch to gurobi by default (if installed) Tim Quatmann 2019-07-26 08:39:20 +0200
  • 88c62d20bf SchedulerClass: setter return a reference to *this Tim Quatmann 2019-07-26 08:37:39 +0200
  • 38795a67b4 PolytopeTree: Better union of childs Tim Quatmann 2019-07-26 08:34:16 +0200
  • e0b2869bd5 Fix region check Jip Spel 2019-07-25 18:26:36 +0200
  • 08d2893b2c Renamed Lattice -> Order Jip Spel 2019-07-25 17:28:09 +0200
  • 1c5d6b7237 Clean up lattice creation code Jip Spel 2019-07-25 16:01:42 +0200
  • 8214c5758e Use parameter lifting for initial ro construction Jip Spel 2019-07-25 13:56:48 +0200
  • adf07416dc Added preservation of time bounded until formulae Alexander Bork 2019-07-25 12:43:04 +0200
  • 34dd9673f1 More statistics. TimQu 2019-07-24 12:26:31 +0200
  • 2a39f8db5d Merge branch 'deterministicScheds' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into deterministicScheds radioGiorgio 2019-07-24 09:21:36 +0200
  • 3820b994c5 product indices getter debugged radioGiorgio 2019-07-24 09:19:39 +0200
  • ad34cbb951 testing radioGiorgio 2019-07-24 09:18:46 +0200
  • a0b7eea500 DetScheds: Print model statistics. TimQu 2019-07-23 17:04:42 +0200
  • b848796852 Nativepolytope: Fixed a bug in quickhull when invoked on just a single point. Tim Quatmann 2019-07-10 12:56:37 +0200
  • 174c1a86c0 DRNParser: Parse labels with and without quotation marks (thanks to pair programming and regex magic Matthias Volk 2019-07-19 14:47:44 +0200
  • 779e5ce5ae DRNParser: Check if target state is valid Matthias Volk 2019-07-19 14:47:01 +0200
  • 976f85cc25 drn export for labels with whitespace is now put into quotation marks Sebastian Junges 2019-07-19 00:10:55 +0200
  • 450e074c5b Integrated non-Markovian state elimination into Storm MA modelchecking Alexander Bork 2019-07-17 17:25:28 +0200
  • 7b038db6d5 Fixed missing part for label preservation and added formula preservation check Alexander Bork 2019-07-17 17:16:45 +0200
  • 31b50d76e9 clearer error message Sebastian Junges 2019-07-17 14:22:48 +0200
  • f2dc42e71c ObjectiveHelper: Fixed wrong rewards with Markov Automata. Tim Quatmann 2019-07-16 18:01:46 +0200
  • a94bc4e284 NativePolytope: More efficient clean operation. Tim Quatmann 2019-07-16 18:01:18 +0200
  • e71033e0e0 LpChecker: Fixed validation of lp results where an objective has weight zero. Tim Quatmann 2019-07-16 18:00:40 +0200
  • 3efee0d35d changelog update: export of mtbdds Sebastian Junges 2019-07-16 16:05:43 +0200
  • 9ad8209a65 clarify that a formula needs to be added to do anything in storm-pomdp Sebastian Junges 2019-07-16 16:04:07 +0200
  • 8838643f98 NativePolytope: Silencing a STORM_LOG_WARN in release mode Tim Quatmann 2019-07-16 14:27:15 +0200
  • 78237e8bb1 LpChecker: Only build the LP model if it is actually needed. Tim Quatmann 2019-07-16 14:26:03 +0200
  • a73c2691b6 Integration of the new settings in the DFT analysis Alexander Bork 2019-07-15 17:41:37 +0200
  • 533206974b proper implemented encoding types. Tim Quatmann 2019-07-15 17:40:14 +0200
  • 5aa19c9a58 Added settings for non-Markovian state elimination Alexander Bork 2019-07-15 17:38:19 +0200
  • b0a3e8bb3a removed choice var reduction and maxdiff encoding Tim Quatmann 2019-07-15 17:30:42 +0200
  • 88d6300084 Added option for label preservation to state elimination Alexander Bork 2019-07-15 17:26:53 +0200
  • 55d8397dca Always use the minnegative encoding. Tim Quatmann 2019-07-15 17:26:42 +0200
  • b8fc1130d1 Statistics via --statistics switch. Tim Quatmann 2019-07-15 17:03:46 +0200
  • 55bf80d434 Validate weight vector checks Tim Quatmann 2019-07-15 16:46:59 +0200
  • 724b2c579e Better statistics output. Tim Quatmann 2019-07-15 16:46:43 +0200
  • 99dd157786 LpChecker: Always do validation. Take result from validation as new point. Tim Quatmann 2019-07-15 15:39:56 +0200
  • b924f15a84 DetScheds: respecting relative precision setting. Tim Quatmann 2019-07-15 15:37:37 +0200
  • ebe249840e Multiobjective: added setting for relative precision and encoding type. Tim Quatmann 2019-07-15 15:36:27 +0200
  • f5b6bc84ba circumvent problems with the bdd export Sebastian Junges 2019-07-12 10:38:05 +0200
  • 4f063cd233 tackling problems on unix Sebastian Junges 2019-07-11 20:36:57 +0200
  • 6ce429efc4 Added missing include Matthias Volk 2019-07-12 10:23:22 +0200
  • ac4687b801 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-11 08:57:42 +0200
  • 13f44ab7ea Monotonicity Checking on Region Jip Spel 2019-07-10 17:45:54 +0200
  • ec67166041 Decoupled preprocessing and SMT solving in commandline interface Alexander Bork 2019-07-10 17:38:57 +0200
  • 449c513db2 Cleanup DFTASFChecker Alexander Bork 2019-07-10 17:03:03 +0200
  • 75d28060cc Moved failure bound computation to decouple it from the SMT checker Alexander Bork 2019-07-10 16:34:18 +0200
  • 85e995c050 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Sebastian Junges 2019-07-10 15:06:52 +0200
  • d295f6e777 export of bdds into dot and text format Sebastian Junges 2019-07-10 15:06:44 +0200
  • 9c74bbed24 Decoupled FDEP conflict search and SMT solver Alexander Bork 2019-07-10 14:34:53 +0200
  • 6402a125b1 MultiobjectivePreprocessorResult: Added a missing linebreak Tim Quatmann 2019-07-10 14:01:17 +0200
  • 5683ffd7bd Merge remote-tracking branch 'origin/master' into deterministicScheds Tim Quatmann 2019-07-10 14:00:49 +0200
  • 52e6149cfd Nativepolytope: Fixed a bug in quickhull when invoked on just a single point. Tim Quatmann 2019-07-10 12:56:37 +0200
  • b190fe6e8f Various bugfixes for deterministic scheds. Tim Quatmann 2019-07-10 12:55:30 +0200
  • bb1e1b2704 Gurobi: Just print an error in case of inaccuracies instead of throwing an exception. Tim Quatmann 2019-07-10 12:53:20 +0200
  • ae5c001d24 Moved non-Markovian state eliminator to its own class Alexander Bork 2019-07-09 18:33:17 +0200
  • 2709b7d828 Merge branch 'master' into dftFDEP Alexander Bork 2019-07-09 17:15:02 +0200
  • 10bb42e0f6 First version of non-Markovian state elimination for MAs Alexander Bork 2019-07-09 14:16:25 +0200
  • 9c52d0d2ab Workaround for IntelTBB linker issue by CMake/Regex magic. Matthias Volk 2019-07-09 10:24:07 +0200
  • 7fb660227f Replaced assert(false) by throwing an exception Matthias Volk 2019-07-04 11:20:04 +0200
  • 685b5c6b27 Throw exceptions after switch/case to silence compiler warnings about not returning anything Matthias Volk 2019-07-04 11:19:24 +0200