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

Commit Graph

  • 275a191b08 Fixed spare claiming by adding missing constraint 'if the child is not claimed at the moment, it will never be claimed'. Matthias Volk 2017-11-24 10:17:41 +0100
  • 7d56572eba Recursive method for generating constrainst for 'trying to claim' Matthias Volk 2017-11-24 10:13:49 +0100
  • e09cb86001 making sure that the default linear equation solver is not switched to native if we check e.g. an MDP with sound value iteration TimQu 2017-11-23 22:45:43 +0100
  • 66d1c828c6 added parametric model checking tests TimQu 2017-11-23 21:49:07 +0100
  • c1b14fc250 increased precision to make a test pass TimQu 2017-11-23 21:48:49 +0100
  • b6d3b0242f Fixed encoding for toplevel element Matthias Volk 2017-11-23 17:38:10 +0100
  • 623ce0ccf1 Fixed missing break in case distinction Matthias Volk 2017-11-23 17:19:04 +0100
  • 1affccbf81 Fixed encoding of PAND Matthias Volk 2017-11-23 16:35:40 +0100
  • 64a0d7ec3a added missing file TimQu 2017-11-23 16:13:22 +0100
  • 1174454ffb Computing upper reward bounds in hybrid dtmc checker TimQu 2017-11-23 16:13:00 +0100
  • 9c6672778b fixed getting/setting the restart threshold in gmmxx environment TimQu 2017-11-23 16:12:06 +0100
  • e46f4e154b 1. Ensured that when doing policy iteration the underlying solver is at least as precise as the minmax solver. 2. Fix for SolverGuarantees: They are only established if bounds were actually given. TimQu 2017-11-23 16:11:08 +0100
  • 3458e42d05 removed a WARN message at wrong position TimQu 2017-11-23 16:07:37 +0100
  • ecb4bdbb4d Redid DTMC and CTMC model checker tests TimQu 2017-11-23 16:06:36 +0100
  • 5ba296404a not finished version of MDP approach Timo Philipp Gros 2017-11-23 12:41:10 +0100
  • d1d2925044 Throw exceptions for missing SMT encodings Matthias Volk 2017-11-22 17:37:58 +0100
  • b567aa0de9 Added encoding for constraint 8 Matthias Volk 2017-11-22 17:26:54 +0100
  • 3df80c3389 Better comments for SMT encoding Matthias Volk 2017-11-22 17:03:34 +0100
  • cf7c09584b Use implication instead off iff in constraint 5 Matthias Volk 2017-11-22 15:42:54 +0100
  • 34911003e0 Better comments for SMT generation Matthias Volk 2017-11-22 15:06:55 +0100
  • 8051912147 Correct indentation Matthias Volk 2017-11-22 13:50:34 +0100
  • dbc18a3eed Merge remote-tracking branch 'upstream/master' Timo Philipp Gros 2017-11-21 10:15:24 +0100
  • 8577b01d1d Merge remote-tracking branch 'upstream/master' into simpleMDPApproach Timo Philipp Gros 2017-11-21 10:08:06 +0100
  • 8421ff5c65 first try, cmake not building Timo Philipp Gros 2017-11-21 09:55:04 +0100
  • 45279f9914 storm-pars compiles now TimQu 2017-11-21 09:30:27 +0100
  • 15a3ad2c2b Merge remote-tracking branch 'origin/master' into environment TimQu 2017-11-21 09:30:12 +0100
  • bb63ac6089 Linear equation solver + game solvers now respect the environment as well TimQu 2017-11-20 20:14:01 +0100
  • dfda3a1544 cleaned up Timo Philipp Gros 2017-11-20 17:51:23 +0100
  • 286fc8aec7 fixed bugs, runnig now Timo Philipp Gros 2017-11-20 16:02:18 +0100
  • c2c306163f slightly fixing syntax dehnert 2017-11-20 13:22:30 +0100
  • 3783ff6420 Fix memory leak in BaseException (and derived exceptions) Joachim Klein 2017-11-20 10:58:17 +0100
  • f5a3291ce7 Fix memory leak in BitVector::operator=(BitVector&& other) Joachim Klein 2017-11-20 10:59:12 +0100
  • f56076aacf Add virtual destructors to classes having virtual functions. Joachim Klein 2017-11-20 10:55:58 +0100
  • 533585fda6 moving to weak_pointers in variables to resolve memory leak in expression manager dehnert 2017-11-20 13:16:23 +0100
  • 253b34ce09 modularised diagonal-prob entrie delete and skipped zero loops in cycle identification Timo Philipp Gros 2017-11-20 08:51:55 +0100
  • fcc997a52d Merge branch 'valueIteration' As trajans is important for both, value iteration and other mdp reachability technique, the seperation of the branch only makes sense AFTER this Timo Philipp Gros 2017-11-19 20:36:47 +0100
  • fe863679bf identify probCycles outgoing states Timo Philipp Gros 2017-11-19 15:26:30 +0100
  • 250fc89bc6 new also supporting Pmin Timo Philipp Gros 2017-11-19 14:01:54 +0100
  • 25a7b6c71a implemented trajans alg to identify prob Cycles Timo Philipp Gros 2017-11-19 12:20:54 +0100
  • 7d65bd5e2e fixing carl version check dehnert 2017-11-17 15:57:00 +0100
  • c20f3a9400 fixed bug in bit vector copy constructor pointed out by Joachim Klein dehnert 2017-11-17 13:00:29 +0100
  • acde9f571f fixed policy iteration on MTBDDs dehnert 2017-11-16 16:34:45 +0100
  • 78842a5005 Fix in symbolic rational search TimQu 2017-11-16 15:38:35 +0100
  • 6911d50985 extended MDP model checker test TimQu 2017-11-16 15:19:06 +0100
  • a47fcbb6f9 making test-solver compile again TimQu 2017-11-16 15:17:58 +0100
  • 9771658dcc only do end component elimination in MDP model checking if there are end components TimQu 2017-11-16 15:17:23 +0100
  • eb272e0125 Merge remote-tracking branch 'origin/master' into environment TimQu 2017-11-16 10:41:54 +0100
  • b10dcce21a fixed 'canHandle' method in pla checker TimQu 2017-11-15 19:28:00 +0100
  • 25c006ec13 fixed method selection of iterative min max solver TimQu 2017-11-15 19:27:39 +0100
  • dea5fb59fe refactored some tests -- making testing with different settings/environments more easy TimQu 2017-11-15 19:27:12 +0100
  • c94bc3a585 fix erroneous copy constructor of bit vector dehnert 2017-11-15 15:52:59 +0100
  • dd9fe2130e bumping xcode version in travis dehnert 2017-11-15 13:41:52 +0100
  • a72f82a6d4 fixed typo dehnert 2017-11-15 11:37:23 +0100
  • 95fae73833 slight improvements to bit vector hashmap dehnert 2017-11-14 22:23:05 +0100
  • 72b9a787e3 Better minmax solver tests TimQu 2017-11-14 18:36:38 +0100
  • 652b69c5b0 Merge remote-tracking branch 'origin/master' dehnert 2017-11-14 17:22:21 +0100
  • 8b557c36a7 adding murmur3 as a possible hash fct for bit vectors dehnert 2017-11-14 16:36:52 +0100
  • 42cea9c688 better subenvironments TimQu 2017-11-14 16:19:38 +0100
  • 4e38d2a13f Merge branch 'master' into ddbisim_partial_quotient dehnert 2017-11-14 15:30:12 +0100
  • 8aecbc356f fixed a test dehnert 2017-11-14 14:42:39 +0100
  • 489800f549 removing superfluous partial bisimulation model checker dehnert 2017-11-14 12:14:10 +0100
  • eaee9bb2c2 removed parallel flag for bisimulation as this is now governed by sylvan:threads already, fixed bug in DD traversal dehnert 2017-11-14 11:52:47 +0100
  • d6c5367e85 fix possible memory leak in bitvector dehnert 2017-11-14 09:00:56 +0100
  • fc28fd16d3 delete self loops for probabilistic states Timo Philipp Gros 2017-11-13 23:25:02 +0100
  • ef7b25d65c Fixed cli settings for storm-dft Matthias Volk 2017-11-13 21:45:49 +0100
  • 03489be59f sligh FNV1a hash improvement dehnert 2017-11-13 20:19:28 +0100
  • e8dc6ee05d applying the same performance improvements for explicit JANI model building dehnert 2017-11-13 19:24:10 +0100
  • 1f9e2967c8 some optimizations in explicit model building dehnert 2017-11-13 16:56:57 +0100
  • dcef30104c storm-pars compiles again TimQu 2017-11-13 13:21:22 +0100
  • 6d23c79737 Making libstorm compile again TimQu 2017-11-13 11:24:53 +0100
  • 0d5a4ef242 more work on sigrefmc integration dehnert 2017-11-12 22:05:10 +0100
  • 99f45fea3c started integrating parallelism implementation of sigrefmc by Tom van Dijk dehnert 2017-11-11 21:42:52 +0100
  • a6046ab0b3 fixed some warnings and issues and introduce cli switch to select IMCA or UnifPlus dehnert 2017-11-11 12:51:51 +0100
  • 0b0b5446cc adding copy constructor TimQu 2017-11-11 10:40:29 +0100
  • a2716ed85b environment in multi-objective model checking methods TimQu 2017-11-11 10:39:56 +0100
  • d0d5217885 implementing destructors in implementation file. TimQu 2017-11-11 08:03:06 +0100
  • 60cf7b5324 Merge branch 'reward-bounded-multi-objective' into environment TimQu 2017-11-11 08:02:28 +0100
  • 54ab1c114e first version of UnifPlus for MA Timo Philipp Gros 2017-11-10 19:46:15 +0100
  • 1d1b17a707 fix some multi-threading issues dehnert 2017-11-10 13:50:41 +0100
  • fd8c99b989 Introducing Environment in MinMaxSolvers and ModelCheckers TimQu 2017-11-10 13:48:50 +0100
  • 05f2f241cb fixed some recently introduced issues dehnert 2017-11-09 20:34:05 +0100
  • d2d129a836 toward multi-threaded dd bisimulation dehnert 2017-11-09 16:39:40 +0100
  • 31ba64f018 bugfixes TimQu 2017-11-09 13:18:11 +0100
  • 94e66a966f removed unused files TimQu 2017-11-09 13:17:21 +0100
  • ccf7521250 Multi-dimensional cumulative reward formulas TimQu 2017-11-09 11:14:16 +0100
  • 9e2dcca5ee extended/improved parsing reward bounded formulas to be compatible with the prism syntax TimQu 2017-11-08 17:55:40 +0100
  • d9e62a66cc cdf export for single objective formulas TimQu 2017-11-08 17:53:31 +0100
  • ace351bd71 Constants wrongfully marked as not graphpresreving. Bugfix for bug reported by Nils Jansen. Sebastian Junges 2017-11-08 15:35:03 +0100
  • edec805e37 added some missing clone functions for check results dehnert 2017-11-08 15:19:47 +0100
  • 45544ddee9 Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-11-08 13:38:13 +0100
  • bdbc6d9c69 fixed typo dehnert 2017-11-07 16:33:59 +0100
  • 4ef0b9eef1 more bug fixes in abstraction-refinement dehnert 2017-11-07 16:01:01 +0100
  • 9b972eef20 some bug fixes in abstraction-refinement dehnert 2017-11-07 14:22:33 +0100
  • 57a6115beb new bisimulation-based abstraction-refinement model checker that uses the new abstraction-refinement framework dehnert 2017-11-07 11:15:33 +0100
  • 8e3e99c4ce fixed bug in submatrix computation pointed out by Timo Gros dehnert 2017-11-06 21:32:06 +0100
  • 330dfb96c7 more work on abstraction-refinement framework dehnert 2017-11-06 16:40:29 +0100
  • 456523b6ec fix missing initialisations sjunges 2017-11-05 22:53:01 +0100
  • b110172b0d fixed bug in MaxSMT-based counterexample generation pointed out by Milan Ceska dehnert 2017-11-03 20:11:32 +0100
  • ce5c740c51 resolved ambiguity to make gcc happy dehnert 2017-11-03 16:31:06 +0100
  • a072ef5310 some fixes to handle large parameters dehnert 2017-11-03 16:06:24 +0100