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

Commit Graph

  • 444f737baa Fix: Returning scaled vector Jan Erik Karuc 2020-02-20 21:23:49 +0100
  • a89c34f9de Actually enable OVI in CLI Jan Erik Karuc 2020-02-20 20:06:43 +0100
  • 94ed2556a8 Center calculation, variables moved for efficiency, removed booleans Jan Erik Karuc 2020-02-20 19:27:24 +0100
  • 4fdfc37341 Factory, Testing Environment (Topological Excluded) Jan Erik Karuc 2020-02-20 18:27:22 +0100
  • 3bd8efd55f CLI option for OVI Jan Erik Karuc 2020-02-20 18:25:48 +0100
  • 761dfc86ea Do not override OVI with SoundIteration Jan Erik Karuc 2020-02-20 18:24:31 +0100
  • cd447aeada Allowing OVI, setting no requirements to be required Jan Erik Karuc 2020-02-20 18:23:22 +0100
  • 323e82994d maixmumElementDiff implementation in vector.h Jan Erik Karuc 2020-02-20 17:47:53 +0100
  • e5e4381eb8 Basic unfinished implementation, reference in header Jan Erik Karuc 2020-02-20 17:44:54 +0100
  • 98bd96eace Merge branch 'master' into portfolio Tim Quatmann 2020-02-20 14:08:17 +0100
  • f7e2ff0843 Apply max. Prog. assumption while building with the dd engine. Tim Quatmann 2020-02-20 12:02:32 +0100
  • ba6f0c0e87 BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption. Tim Quatmann 2020-02-20 12:01:55 +0100
  • 9e54ce4e8b Improved detection of terminal states for Dd engine. Also reduced code duplication. Tim Quatmann 2020-02-19 15:29:37 +0100
  • 0060e594c0 Added Missing includes. Tim Quatmann 2020-02-19 10:09:30 +0100
  • 066593f4c1 Updated Changelog. Tim Quatmann 2020-02-18 15:28:21 +0100
  • c66b0ea442 model-handling: Fixed compatibility checks Tim Quatmann 2020-02-18 15:28:10 +0100
  • bb3f7c52fd DdJaniModelBuilder: Fixed canHandle Tim Quatmann 2020-02-18 15:27:40 +0100
  • 77c3c37e3c Implemented portfolio decisions Tim Quatmann 2020-02-18 15:06:04 +0100
  • 1e8a12170d FormulaInformation: Also track whether a formula contains a long-run average formula Tim Quatmann 2020-02-18 15:05:37 +0100
  • 54b37d8698 Added entry points for portfolio engine Tim Quatmann 2020-02-18 13:48:56 +0100
  • c6c6f45483 Fixed compilation for storm-pars and storm-pomdp Tim Quatmann 2020-02-18 13:48:25 +0100
  • 4da25662f8 Engine: check whether an engine can handle the query given by a model and a *list* of properties Tim Quatmann 2020-02-18 10:22:27 +0100
  • 8711b32c99 When using bisimulation with the dd-to-sparse engine, the quotient is automatically extracted in a sparse way. Tim Quatmann 2020-02-18 09:06:16 +0100
  • 1574f4444a CLI: Introduced ModelProcessingInformation which allows to set certain settings (regardinge model building and model verification) in an on-the-fly manner. Tim Quatmann 2020-02-18 09:05:14 +0100
  • a99f0905e2 dd/bisimulation: Added argument to "getQuotient" which allows to set the quotient type (dd / sparse) Tim Quatmann 2020-02-18 08:49:52 +0100
  • ead5845686 BuilderType: Using new canHandle and getSupportedJaniFeatures methods. Tim Quatmann 2020-02-17 14:28:23 +0100
  • 23fb3bedff all model builders: Added a canHandle method and a getSupportedJaniFeatures method. Tim Quatmann 2020-02-17 14:26:57 +0100
  • ac35a04eec utility/engine: canHandle(...) compiles now. Moved getSupportedJaniFeatures to builder/BuilderType. Tim Quatmann 2020-02-17 12:01:24 +0100
  • 739151af8d CLI: Provide the engine as a parameter in most of the CLI options. Tim Quatmann 2020-02-17 11:58:33 +0100
  • 17325419fb Introduced JIT as a separate engine. Tim Quatmann 2020-02-17 10:49:45 +0100
  • d9176dc867 all (core) modelcheckers: Devided the canHandle method into a static and a non-static part. This allows to detect incompatibility before building the model. Tim Quatmann 2020-02-17 09:29:51 +0100
  • 18bfe74d8f api/model_descriptions: Fixed ambiguous method declaration. Tim Quatmann 2020-02-17 09:28:02 +0100
  • 85bf82fcef storm-pars: Removed redundant include. Tim Quatmann 2020-02-17 09:26:04 +0100
  • 0a7119cd56 Merge branch 'master' into portfolio Tim Quatmann 2020-02-14 12:31:09 +0100
  • 5f18704bec Added makeOptional to arguments of the --qvbs option. Tim Quatmann 2020-02-14 12:30:58 +0100
  • d36cd93ae8 CLI: Split parsing and preprocessing of symbolic input into two steps. Moved engine related methods and declaration to a separate file. Tim Quatmann 2020-02-14 12:30:12 +0100
  • 91232a2b11 Changed data structure for belief distributions from vector to map to exploit sparsity Alexander Bork 2020-02-11 16:11:42 +0100
  • 6891825803 IterativeMinMaxLinearEquationSolver: Fixed not incrementing an iterator when computing the maximum absolute difference between two values Tim Quatmann 2020-02-10 15:18:39 +0100
  • cec2fd420a Fixed compiler warning Matthias Volk 2020-02-07 17:40:47 +0100
  • 9e13f42a03 fix in permute when no rowgroupindices where given Sebastian Junges 2020-02-07 15:57:00 +0100
  • 863aebaa2a add flag for canonicity Sebastian Junges 2020-02-07 15:56:40 +0100
  • 03de01f54e support for make canonic if no choice origins are available Sebastian Junges 2020-02-07 12:08:32 +0100
  • 112973d02a adapt for hintsettings that have been added recently Sebastian Junges 2020-02-07 12:07:13 +0100
  • fe21001eb3 Merge branch 'master' into pomdp-building Sebastian Junges 2020-02-06 17:53:46 +0100
  • 0a6f54f33e a version of parsing choice labels from DRN Sebastian Junges 2020-02-06 16:41:37 +0100
  • f322149398 export the number of choices into drn Sebastian Junges 2020-02-06 14:58:34 +0100
  • debabb01bb cmd line arguments for hinting on the number of states added Sebastian Junges 2020-02-06 14:54:48 +0100
  • 9cd5a4e657 first version of the information collector for jani files Sebastian Junges 2020-02-06 14:30:35 +0100
  • 6147b35fc8 collect number of variables Sebastian Junges 2020-02-06 14:28:22 +0100
  • c845c10ee6 added a test for new pomdp stuff Sebastian Junges 2020-02-05 17:36:45 +0100
  • d398d6643f enable logging Sebastian Junges 2020-02-05 17:35:40 +0100
  • 0d5d3774d2 changelog updated with pomdp changes Sebastian Junges 2020-02-05 17:35:06 +0100
  • 3051559ea8 Output on failure for tests Matthias Volk 2020-01-31 16:44:25 +0100
  • a082e7d228 Typos Matthias Volk 2020-01-31 16:41:35 +0100
  • c8158018b8 Use state elimination to eliminate chains of non-Markovian states in MA Matthias Volk 2020-01-31 16:41:19 +0100
  • 9fc473383f Cosmetic changes in BitVector. Matthias Volk 2020-01-31 00:14:21 +0100
  • 544dd60206 Removal of labels Matthias Volk 2020-01-30 22:37:33 +0100
  • 1fe1bd4dea various diagnostic informations to explain why we reject a POMDP Sebastian Junges 2020-01-25 20:03:30 +0100
  • cb2e22e1d3 improved error message if observables includes an unknown error variable Sebastian Junges 2020-01-25 20:02:47 +0100
  • 09cf1902e0 added transformer to make pomdp canonic Sebastian Junges 2020-01-25 13:43:14 +0100
  • b554dabaab state generator now takes into account observable expressions when building POMDPs Sebastian Junges 2020-01-25 13:34:59 +0100
  • 9469e9b088 added missing settings Sebastian Junges 2020-01-25 13:28:34 +0100
  • 7bebb18250 bitvector concat and expand Sebastian Junges 2020-01-25 12:37:27 +0100
  • 290ede7404 extended the parser to handle observable expressions Sebastian Junges 2020-01-24 18:27:49 +0100
  • e177a5420a added observation labels to the prism program Sebastian Junges 2020-01-24 18:26:47 +0100
  • 95b2c829f1 introduced observation labels in prism Sebastian Junges 2020-01-24 18:25:42 +0100
  • be3ff1520f export in api can be called without explicitly giving parameter names Sebastian Junges 2020-01-24 18:24:18 +0100
  • be063dba14 POMDPs are now always built with choice labelling and choice indices Sebastian Junges 2020-01-24 18:23:32 +0100
  • a53b7ca005 permute actions in reward models Sebastian Junges 2020-01-24 18:21:57 +0100
  • 340be99e78 permutation of items Sebastian Junges 2020-01-24 18:21:20 +0100
  • 8a7e40558d permute for matrices Sebastian Junges 2020-01-24 18:20:24 +0100
  • 0dd15b4e2f permute for bitvectors Sebastian Junges 2020-01-24 18:19:21 +0100
  • a58ec3fd5f permutations for vectors Sebastian Junges 2020-01-24 18:18:01 +0100
  • e02ea57a58 Rudimentary version of the refinement loop Alexander Bork 2020-01-24 17:08:46 +0100
  • a5fc9fc5b7 Added naive underapproximation by unrolling the belief support up to a given size Alexander Bork 2020-01-24 11:05:25 +0100
  • 003d2024c1 Restored functionality of --firstdep Matthias Volk 2020-01-22 16:03:04 +0100
  • 8e24f141f9 Initial label is kept in NonMarkovianChainElimination with heuristic 'delete' Matthias Volk 2020-01-22 11:11:47 +0100
  • 8073a6d989 Fix in DFTs to translate MAs to CTMCs again Matthias Volk 2020-01-22 10:58:06 +0100
  • 4bbb02dcaa Wrong method for underapproximation for future reference Alexander Bork 2020-01-20 10:37:03 +0100
  • ee3c08a085 Set floating-point precision to 10 digits for file export Matthias Volk 2020-01-14 12:52:24 +0100
  • 33917f3510 Made argument for '--progress' optional Matthias Volk 2020-01-13 17:35:26 +0100
  • abdbef06f6 Enabling GLPK MILP Presolver by default (again) Tim Quatmann 2020-01-13 14:14:13 +0100
  • 3760824fc1 DetSchedsLpChecker: Sharpen constraints if the LP solver was inaccurate. Tim Quatmann 2020-01-13 14:11:33 +0100
  • 575642c688 MultiObjectiveSettings: Made an argument optional. Tim Quatmann 2020-01-10 15:18:08 +0100
  • 8719dd8f71 GlpkLpSolver: Added a command line option to enable MILP presolving. Tim Quatmann 2020-01-10 15:11:36 +0100
  • 03a77f9c6a Added new Gurobi version Tim Quatmann 2020-01-09 13:07:06 +0100
  • a73035efdf Added some document explaining how one can build a package for offline installation of storm. Tim Quatmann 2020-01-09 13:06:47 +0100
  • 61a99a9b9d Consistent use of printInfo in DFTModelChecker Matthias Volk 2020-01-07 19:51:21 +0100
  • a647383d94 Extended help message for --ec-label-behavior Matthias Volk 2020-01-07 19:28:43 +0100
  • 607e4594da Merge from master Matthias Volk 2020-01-07 17:32:41 +0100
  • 605546358b Added option to merge labels of eliminated states into existing states Alexander Bork 2019-11-15 10:11:35 +0100
  • 6a321acae7 Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp Alexander Bork 2020-01-07 14:30:21 +0100
  • e490a0ba52 Fixed iteration over all labels Alexander Bork 2020-01-07 14:29:45 +0100
  • 37781a688b Added makeOptional()s in MultiObjectiveSettings Tim Quatmann 2020-01-06 16:25:00 +0100
  • 858e2f8a60 various improvements and fixes in winning region computation Sebastian Junges 2020-01-02 16:45:34 +0100
  • aae8774e5f added options, allow to toggle output Sebastian Junges 2019-12-21 23:15:14 +0100
  • 3f4bb4cf8d we now compute the winning region Sebastian Junges 2019-12-21 22:05:10 +0100
  • 93ed0224a1 options for searching for qualitative schedulers Sebastian Junges 2019-12-21 22:03:36 +0100
  • 9a5b01b6f7 a new encoding for almost sure reachability Sebastian Junges 2019-12-21 17:32:21 +0100
  • 86f5cda3d4 Merge branch 'master' into prism-pomdp Sebastian Junges 2019-12-19 11:08:03 +0100