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

Commit Graph

  • f88ee9d9ae fixed compilation of gmmxx multiplier and sparseMatrix with intel tbb enabled TimQu 2018-09-24 15:25:09 +0200
  • 5a0f135cc8 Merge remote-tracking branch 'origin/master' into jani-arrays TimQu 2018-09-24 15:24:40 +0200
  • b23627bf7e Merge remote-tracking branch 'origin/master' into jani-arrays TimQu 2018-09-24 15:24:21 +0200
  • 29f9275302 Refactor validation methods Jip Spel 2018-09-24 14:46:56 +0200
  • b82ab5f9c2 Validate assumption with SMT solving Jip Spel 2018-09-24 13:39:51 +0200
  • 83cb103177 Change variable naming Jip Spel 2018-09-24 13:36:56 +0200
  • 42f49d8914 support for carl:c++14 tag Sebastian Junges 2018-09-23 22:09:37 +0200
  • 64b0360d79 improved runtime of jani JSONExporter TimQu 2018-09-21 14:23:53 +0200
  • a2f1ed9985 when converting prism formulas to jani functions, only variables that appear in a module renaming are taken as a parameter TimQu 2018-09-21 14:22:48 +0200
  • b08373ac67 fixed in reward accumulation elimination of total reward formulas TimQu 2018-09-21 14:21:57 +0200
  • 10662e92eb fixed an issue related to transient assignments in the 'wrong' order TimQu 2018-09-20 17:42:17 +0200
  • c95ca4ed15 All model builders support state-exit rewards TimQu 2018-09-20 16:34:20 +0200
  • 0bacb6f5eb fixed incorrect parsing of jani constants TimQu 2018-09-20 16:33:55 +0200
  • 14875e9067 removed debug output TimQu 2018-09-20 15:12:48 +0200
  • 0dcfd41f87 fixed appending to existing files in jani export TimQu 2018-09-20 15:10:45 +0200
  • e2cb1dd78a fixed ToJaniConverter for the case where not all variables are global TimQu 2018-09-20 15:09:55 +0200
  • bb04291860 fixed parsing of jani-function: two passes are required as functions can be defined before they are used TimQu 2018-09-20 15:09:23 +0200
  • a95331948c fixed operator<< of function call expr TimQu 2018-09-20 14:14:29 +0200
  • ee9e6354a3 removed standard-compliant option: storm-conv now produces standard compliant jani code by default TimQu 2018-09-20 14:12:49 +0200
  • 9375709381 Split validate into two methods Jip Spel 2018-09-20 14:03:16 +0200
  • 13bc33328a fix in toJaniConverter TimQu 2018-09-20 13:59:58 +0200
  • a243a69aa6 Create test for MonotonicityChecker Jip Spel 2018-09-20 12:49:50 +0200
  • d99e728add Add return to check monotonicity Jip Spel 2018-09-20 12:48:16 +0200
  • 58dc2512cf Create test for AssumptionMaker Jip Spel 2018-09-20 11:31:44 +0200
  • 712faae653 Create test for LatticeExtender Jip Spel 2018-09-20 11:06:20 +0200
  • 705d8ecc1a Create test for Lattice Jip Spel 2018-09-20 10:26:39 +0200
  • c81319135d Make enum for constants Jip Spel 2018-09-20 10:22:46 +0200
  • 646b668bd4 Added a new mdp model checker test TimQu 2018-09-20 10:09:20 +0200
  • f50f1c2ee4 Fixed parsing of jani function definitions TimQu 2018-09-20 10:00:45 +0200
  • ea1a1d97ef fixed export of jani functions to json. Remove output to cout when writing the jani file TimQu 2018-09-20 09:59:27 +0200
  • c3837968dd nicer output for storm-conv and fixed an issue in storm-conv related to substituting constants before translating the functions TimQu 2018-09-20 09:58:49 +0200
  • ccb5a89de3 Formula substitutions need to be performed before constant substitutions because otherwise, constants appearing in formula expressions can not be handled properly TimQu 2018-09-20 09:55:56 +0200
  • aaae25ee76 Update AssumptionCheckerTest Jip Spel 2018-09-20 09:28:43 +0200
  • 71408bc011 Setup test for AssumptionChecker Jip Spel 2018-09-19 16:44:25 +0200
  • 0e0f2c2390 fixed substitution of prism formulas TimQu 2018-09-19 16:22:08 +0200
  • 5f9949bfbf reduce nesting for jani expressions TimQu 2018-09-19 14:39:09 +0200
  • ce231fd927 Fix assert in Lattice Jip Spel 2018-09-19 16:09:20 +0200
  • 7f799ecb28 Fixed return of local variable Matthias Volk 2018-09-19 14:39:10 +0200
  • 4ccc837434 Fixed setting correct model type for JaniGSPNBuilder Matthias Volk 2018-09-19 14:38:57 +0200
  • 90095a5455 correct conversion of prism formulas to jani functions when modules were renamed TimQu 2018-09-19 14:28:25 +0200
  • 6e2046e357 fixed formula substitution within renamed modules of a prism program TimQu 2018-09-19 14:27:41 +0200
  • c388d1c8fe making sure that functions in jani models and formulas in prism programs are substituted before flattening the model TimQu 2018-09-19 14:18:42 +0200
  • 24abcfb61c AssumptionChecker for mdp Jip Spel 2018-09-19 09:14:10 +0200
  • 4d74ec501a substitute formulas in properties after parsing TimQu 2018-09-19 08:55:56 +0200
  • 82931f3390 Add asserts to Lattice Jip Spel 2018-09-19 08:35:48 +0200
  • 71489a24f5 The model builders now substitute jani functions (if still present) TimQu 2018-09-18 22:58:33 +0200
  • 487f370c58 fixed getting the function identifier TimQu 2018-09-18 22:54:51 +0200
  • a173cb68b8 fixed some janibuilder tests TimQu 2018-09-18 22:45:51 +0200
  • aa6fd3cbb2 fixed compilation of storm-conv TimQu 2018-09-18 22:45:26 +0200
  • 340c7f0db7 fixed getting the function identifier TimQu 2018-09-18 22:45:01 +0200
  • 55efedb713 prism2jani no longer fails if a reward model has the same name as a formula/variable TimQu 2018-09-18 22:40:05 +0200
  • 032d68b9b0 switching to recursive synchronization resolution for JANI explicit model exploration dehnert 2018-09-18 22:40:53 +0200
  • 1b7f150e76 implemented functionality to rename reward model names TimQu 2018-09-18 22:17:19 +0200
  • 2dd5c65051 fixed duplicated symbol linker error TimQu 2018-09-18 22:16:29 +0200
  • 1190f32b56 cleanup in jani parser TimQu 2018-09-18 22:16:09 +0200
  • 205ed7f4bf special treatment of trivial initial states restriction for JANI (following PRISM) next-state generator dehnert 2018-09-18 20:48:26 +0200
  • 23edcc1a75 Refactor AssumptionChecker Jip Spel 2018-09-18 17:38:20 +0200
  • f89817da3b eliminating reward accumulations directly at parsing time TimQu 2018-09-18 15:45:20 +0200
  • 28d4dd481d simplified processing of janiConversionOptions TimQu 2018-09-18 15:43:34 +0200
  • 101b49b898 detect unsupported jani-features directly upon parsing the model. TimQu 2018-09-18 15:42:48 +0200
  • ae1987f64c Function and array eliminator now do not perform any action, if the corresponding model feature is not enabled TimQu 2018-09-18 15:38:52 +0200
  • 4453eb4134 substitute jani-functions during preprocessing (analogous to prism program preprocessing) TimQu 2018-09-18 15:34:18 +0200
  • e85b9759e2 better parsing of model features TimQu 2018-09-18 15:32:15 +0200
  • ede671ea3f fixed wrong type mask for arrays... TimQu 2018-09-18 15:30:55 +0200
  • 90c9e95c8a Only consider the reachable set of states after closing an MA TimQu 2018-09-18 15:30:32 +0200
  • 285cde32ae Also give result when lattice does not contain all states Jip Spel 2018-09-18 14:40:18 +0200
  • 034fbf20c7 extended SubsystemBuilder, made ChoiceSelector work for MAs as well. TimQu 2018-09-18 14:39:32 +0200
  • b20a7efe12 Replace dummy code Jip Spel 2018-09-18 13:47:06 +0200
  • 4afa6d8a0f Make validation of assumptions optional Jip Spel 2018-09-18 13:19:44 +0200
  • 11776a822a Add documentation Jip Spel 2018-09-18 12:51:39 +0200
  • 24a40bba80 Add validated assumptions to set Jip Spel 2018-09-18 12:08:53 +0200
  • e23a222605 Add simple validation for assumptions Jip Spel 2018-09-18 10:30:59 +0200
  • bdeacf8669 better treatment of cases where array out of bounds accesses occurr TimQu 2018-09-18 10:10:49 +0200
  • 7bae50d0ba fixed correct parsing of prism formulas TimQu 2018-09-18 10:06:23 +0200
  • 10ae6a0dd8 fixed not respecting negative assignment indices in array eliminator TimQu 2018-09-17 09:57:48 +0200
  • 8836e7a676 made pgcl2jani and gspn2jani compile again TimQu 2018-09-17 09:41:31 +0200
  • 5e43c51f49 starting on some builder optimizations dehnert 2018-09-16 21:49:16 +0200
  • 092a43a0a5 fixed correct export of modulo operator TimQu 2018-09-15 11:52:19 +0200
  • d47189f93e fixes for array elimination TimQu 2018-09-15 11:29:25 +0200
  • 5dda7a5296 removed unused file 'variable substitution visitor' TimQu 2018-09-14 17:04:29 +0200
  • b5bb87404c replaced occurrences of 'substituteConstants' by 'substituteConstantsFormulas' TimQu 2018-09-14 17:03:53 +0200
  • 7af70a77aa slight fix to bit vector sizes used in explicit model builder dehnert 2018-09-14 17:01:20 +0200
  • c052da15b9 conversion from prism to jani respects formulaas TimQu 2018-09-14 16:56:03 +0200
  • 3cf9553126 actually fixed model feature support TimQu 2018-09-14 16:54:01 +0200
  • ea76f6d0be prism parser no longer inserts formula definitions directly. Note that these have to be eliminated afterwards TimQu 2018-09-14 16:40:18 +0200
  • 6d5af2d414 fixed exporting model-features TimQu 2018-09-14 16:38:13 +0200
  • 78d98655f6 gspn and pgcl jani model builders now correctly add the model feature 'derived-operators' TimQu 2018-09-14 16:35:07 +0200
  • e119131f78 storm-conv compiles TimQu 2018-09-14 16:34:37 +0200
  • c739f0befa elimination of jani function TimQu 2018-09-14 15:38:05 +0200
  • f2c2da64fa Add documentation LatticeExtender.h Jip Spel 2018-09-14 13:16:37 +0200
  • e4a2e9ffad Update documentation Lattice.h Jip Spel 2018-09-14 13:06:48 +0200
  • 8bded41867 Add state to lattice when there are more than 2 outgoing transitions Jip Spel 2018-09-14 13:00:12 +0200
  • edc21be6ec Add comments Jip Spel 2018-09-14 11:53:41 +0200
  • 240f81dfcb Clean up MonotonicityChecker Jip Spel 2018-09-14 11:34:24 +0200
  • 3fcf4f83c0 Clean up AssumptionMaker Jip Spel 2018-09-14 11:31:21 +0200
  • fba6fe76b5 Clean up AssumptionChecker Jip Spel 2018-09-14 11:30:59 +0200
  • 06255ef08e Use BinaryRelationExpression to check on samples Jip Spel 2018-09-14 11:06:28 +0200
  • bb92be14dc fixes for array translation TimQu 2018-09-14 09:28:21 +0200
  • b1272c58b6 Parsing and exporting of jani-functions TimQu 2018-09-14 08:58:26 +0200
  • 2febe36a65 removed dependency on storm-conv TimQu 2018-09-14 08:54:46 +0200