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

Commit Graph

  • 8fe3b7b1f8 give edges a color to mark them from user side Sebastian Junges 2018-10-10 19:53:21 +0200
  • f2850f9e6f verification api now takes (optionally) the environment as a first parameter, to make code less dependent on global setttings objects Sebastian Junges 2018-10-10 19:52:53 +0200
  • e8e87d26d6 Add check if result actually contains the given variable Jip Spel 2018-10-10 13:48:28 +0200
  • 87fa9908bf Fixed an issue where scheduler generation in MDPs was not possible due to end components even if there actually were no end components. TimQu 2018-10-10 13:32:32 +0200
  • d64ba97d2f Change bounds to strictly greater/smaller Jip Spel 2018-10-10 12:56:26 +0200
  • 229ce127e6 Fix TODO and improve initial check on samples Jip Spel 2018-10-10 09:48:50 +0200
  • 2b1ef118d3 fixed a few cases where an exportet jani file may contain 'null' TimQu 2018-10-10 09:12:12 +0200
  • 90e9d91530 add undefined constants in properties to the jani model when converting TimQu 2018-10-10 09:11:39 +0200
  • fccd9851e7 Merge branch 'ptas' TimQu 2018-10-09 16:34:19 +0200
  • d7ec0b65e8 Conversion of Prism PTAs to Jani PTAs TimQu 2018-10-09 16:33:06 +0200
  • c5ef182002 added PTA features (clock variables, location invariants) for jani TimQu 2018-10-09 16:32:34 +0200
  • 2b90975525 parsing prism PTAs TimQu 2018-10-08 16:24:42 +0200
  • 37eb90bc82 better check whether transition rewards can be scaled and lifted to action rewards TimQu 2018-10-08 12:02:04 +0200
  • e3c0a49ed3 New RewardModelInformation now compiles... TimQu 2018-10-08 12:01:22 +0200
  • f098daf2f3 Add stopwatches Jip Spel 2018-10-08 11:40:14 +0200
  • cca2ad474e First check on samples for monotonicity Jip Spel 2018-10-08 11:12:15 +0200
  • 0a6122258c Used the new reward information traverser wherever one needs to find out the reward kinds of a given rewardmodel TimQu 2018-10-08 10:06:29 +0200
  • 793228c150 Added a traverser that finds out, whether a given reward model has state/action/transition rewards TimQu 2018-10-08 10:03:32 +0200
  • 8c7808b0df No need to check for state breaking the SCC Jip Spel 2018-10-08 09:09:36 +0200
  • 5a438991e2 Delete lattice when assumption is not valid Jip Spel 2018-10-08 09:07:58 +0200
  • 334bcfd977 removed some tests to reflect new behavior of JANI compositions may refer to unknown actions dehnert 2018-10-06 16:20:14 +0200
  • 8213790089 Merge remote-tracking branch 'origin/master' into janiTests dehnert 2018-10-06 15:22:44 +0200
  • acfb8d28c0 fixing issues related to rewards in JIT-based model builder dehnert 2018-10-06 15:22:32 +0200
  • fd6452e6a4 correcting test dehnert 2018-10-05 22:21:19 +0200
  • e745ddbe0d some fixes related to DD-based JANI model building dehnert 2018-10-05 21:13:13 +0200
  • 5bafcbe816 prism to jani: return properties also in simple cases Sebastian Junges 2018-10-05 17:59:46 +0200
  • 4adcc5c8a5 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Sebastian Junges 2018-10-05 17:50:37 +0200
  • a48f90a523 Guard setInitialStates with hasInitialStatesRestriction Sebastian Junges 2018-10-05 17:29:11 +0200
  • 4e9ae0823e JaniParser: fixed parsing of integer variables without initial value TimQu 2018-10-05 15:05:09 +0200
  • 59afd1375a Update documentation Jip Spel 2018-10-05 13:53:06 +0200
  • 901105f9e4 Only divide by denominator when function is not constant Jip Spel 2018-10-05 13:44:21 +0200
  • eab6a9e38a Distinguish between validated and valid in AssumptionChecker and AssumptionMaker Jip Spel 2018-10-05 11:49:14 +0200
  • 98f1468479 remove constant from model, e.g. for constants that do not appear in the model Sebastian Junges 2018-10-04 22:49:03 +0200
  • 9d78c8d22c jani set model type, useful to change from dtmc to mdp semantics -- be careful in usage though Sebastian Junges 2018-10-04 22:48:05 +0200
  • 41e7932b18 jani exporter: dont write null if no properties are given Sebastian Junges 2018-10-04 22:47:19 +0200
  • 7f5d159154 fix spurious semicolon warning sjunges 2018-10-04 22:35:03 +0200
  • d417c9ecbe Fix assertion. assert(x < y < z) is not the same as assert(x < y and y < z). sjunges 2018-10-04 22:14:14 +0200
  • ad1a842798 Merge branch 'master' into dft_smt Matthias Volk 2018-10-04 20:42:03 +0200
  • 97b248ec8f Updated changelog TimQu 2018-10-04 10:28:03 +0200
  • 03c80f3ae1 correct treatment of non-trivial reward expressions TimQu 2018-10-04 10:27:43 +0200
  • 6102fd27ae Subsystembuilder can now handle deadlock states TimQu 2018-10-04 10:26:32 +0200
  • cc78629dda refer to storm-pomdp in changelog Sebastian Junges 2018-10-02 18:58:52 +0200
  • 035bbd0952 removed spurious debugging output Sebastian Junges 2018-10-02 18:53:44 +0200
  • fef4b694d4 topo sort: add first states Sebastian Junges 2018-10-01 16:36:24 +0200
  • 28b06f5eda Add another way to extend the lattice Jip Spel 2018-10-02 16:47:53 +0200
  • 54a7c84725 started fixing some issues related to transient variable assignments in DD-based JANI model builder dehnert 2018-10-02 15:50:46 +0200
  • 03044af131 Merge branch 'master' into janiTests dehnert 2018-10-02 13:17:53 +0200
  • 3811c3f0b4 converting error on missing action in JANI DD-builder to warning dehnert 2018-10-02 09:27:31 +0200
  • 8332abab58 Removed unused variables Matthias Volk 2018-10-01 16:42:27 +0200
  • eb6fa09ef8 Fixed warning for initialization order Matthias Volk 2018-10-01 16:39:20 +0200
  • 2e7569eea4 Merge branch 'master' into pomdp_datastructures Sebastian Junges 2018-10-01 16:01:37 +0200
  • 1074259b6d Merge branch 'master' into pomdp_datastructures Sebastian Junges 2018-10-01 16:01:04 +0200
  • 88c6b4d66b Ignore self loops in lattice creation when there are several outgoing transitions Jip Spel 2018-10-01 14:40:47 +0200
  • c85da52e8b Give message when no lattices are created Jip Spel 2018-10-01 14:07:08 +0200
  • 67862b0a8d First implementation for cyclic parts in model Jip Spel 2018-10-01 14:05:56 +0200
  • eb8240bfff Add message when no parameters occur in final model Jip Spel 2018-10-01 13:52:44 +0200
  • a37c42d7dc Fix same name parameter Jip Spel 2018-10-01 13:43:57 +0200
  • 0588fb0cc0 Travis: Workaround for nonblocking mode Matthias Volk 2018-10-01 13:07:36 +0200
  • c6204254a3 fixing two issues related to complex model building and in particular integer vs rational division dehnert 2018-09-29 13:08:02 +0200
  • 24cf45d9b6 prism ToJaniConverter now adds the 'state-exit-rewards' model feature if present TimQu 2018-09-28 16:40:17 +0200
  • bb7f4dd6d7 canHandle method of exact continuous time model checkers now return 'false' for time-bounded properties TimQu 2018-09-28 16:39:37 +0200
  • 7f6823c6bb Resolve TODO Jip Spel 2018-09-28 13:22:05 +0200
  • 4fb3f68a94 Added inhibitor arcs for spare, fixing boundedness with merged places + TODO Dependency priority fixing Alexander Bork 2018-09-28 11:52:57 +0200
  • 4d7246fbd6 Merge branch 'master' into janiTests TimQu 2018-09-27 14:24:52 +0200
  • 4dc234d635 silenced several 'unused parameter'-warnings TimQu 2018-09-27 14:24:09 +0200
  • 86d99d8ca5 silenced a few warnings TimQu 2018-09-27 13:55:57 +0200
  • 09efbcff34 fixed a test TimQu 2018-09-27 11:57:16 +0200
  • 01b5751891 Merge branch 'master' into janiTests TimQu 2018-09-27 11:55:51 +0200
  • bf40fb54f2 added api call that directly applies a given jani-property filter TimQu 2018-09-27 11:46:35 +0200
  • 8c37d4eade conversion input settings now properly take a jani property filter TimQu 2018-09-27 11:45:45 +0200
  • ebfee78ecc Fixed compilation of tests TimQu 2018-09-27 11:44:35 +0200
  • 3ab4a28db1 fixing bug triggered by one of Steffen's (TUD) input models dehnert 2018-09-26 21:54:16 +0200
  • ec3881e502 Merge branch 'master' into janiTests TimQu 2018-09-26 20:51:28 +0200
  • 858de4bf48 'applyUpdate' in jani next state generator now works in-place TimQu 2018-09-26 20:49:54 +0200
  • f8a442ae0b clean-up of jani next state generator TimQu 2018-09-26 20:39:10 +0200
  • 019cc8b1a0 preserved order of jani-properties as given in the file TimQu 2018-09-26 20:38:55 +0200
  • 31a67afa4a also print filtered rationalNumber checkresults as double TimQu 2018-09-26 19:53:32 +0200
  • 6dec8ca659 Increased precision of parsing of floating point numbers TimQu 2018-09-26 14:39:00 +0200
  • c1f85b0fac improved the assignmentsFinder a little TimQu 2018-09-26 14:09:45 +0200
  • 287fdce9d5 fixed issue related to having assignment levels and edge assignments at the same time TimQu 2018-09-26 14:09:17 +0200
  • 6e37bd3271 fixed an issue with building MAs via jit TimQu 2018-09-26 12:58:21 +0200
  • 02fdc292fd handling non-trivial reward expressions in jani-builders TimQu 2018-09-26 12:57:46 +0200
  • d3952c82f6 fix in variable information for unbounded variables TimQu 2018-09-26 12:53:50 +0200
  • 7cdbd257d3 support for parsing/storing/exporting non-trivial reward expressions TimQu 2018-09-26 12:52:41 +0200
  • 6695f64460 Add test and fix bug RationalFunction to Expression Jip Spel 2018-09-26 10:48:42 +0200
  • bdad601501 Validate assumption with SMT Solver - more than 2 successor states Jip Spel 2018-09-26 10:37:43 +0200
  • 4cda27f094 jani next state generator now sets values of transient variables in the evaluator to evaluate reward expressions TimQu 2018-09-25 15:20:52 +0200
  • d875f8ba0d lowest/highest assignment level of an edge now only consider the edge destinations TimQu 2018-09-25 15:14:39 +0200
  • fed5b0d81b Added support for transient variables on the rhs of an assignment TimQu 2018-09-25 13:45:43 +0200
  • 5a36fa0075 Expression evaluator can now set rational values from a RationalNumber/RationalFunction TimQu 2018-09-25 13:45:13 +0200
  • b8b84e3f8a support for *local* unbounded integer variables. TimQu 2018-09-25 13:44:33 +0200
  • 4999ac5440 Check if derivative is constant in validation of assumption Jip Spel 2018-09-25 13:41:40 +0200
  • 51aace8421 Renamed ValueTypeToExpression to RationalFunctionToExpression Jip Spel 2018-09-25 13:15:35 +0200
  • c9c2816e18 Add documentation Jip Spel 2018-09-25 11:29:27 +0200
  • 440b127880 Add test for ValueType to Expression Jip Spel 2018-09-25 11:11:14 +0200
  • 4d1dfdc75c Fix problem with exponent and denominator Jip Spel 2018-09-25 11:10:05 +0200
  • 949bc4cb65 Fixed bugs in jani next state generator introduced during merge TimQu 2018-09-24 22:11:30 +0200
  • 5ab404a9d3 added support for unbounded integer variables in explicit jani builder such that it is treated as a bounded variable (with a given number of bits) and an exception is thrown in case of an underflow or overflow TimQu 2018-09-24 18:05:14 +0200
  • a2189044f3 Use degree of variable in expression Jip Spel 2018-09-24 16:45:31 +0200
  • e7c0bd0f7d array variables can now have only a lower (or upper) element type bound TimQu 2018-09-24 16:09:44 +0200