Commit Graph

  • d2cd142dfb Fixed initial partitioning in sparse bisimulation with action-based rewards. TimQu 2018-11-27 20:36:37 +0100
  • 8a7a604f4c Fixed actually taking options for non-deterministic bisimulation when performing non-deterministic bisimulation. TimQu 2018-11-27 20:34:57 +0100
  • 985319c7dd Tweaked LRA computation for MDPs and MAs in sound mode to meet precision requirements. TimQu 2018-11-27 15:11:59 +0100
  • 5d61329eb3 SVI with relative precision computed values that were unnecessarily precise. TimQu 2018-11-27 15:11:18 +0100
  • a302ec9cfc Fix in BucketPriorityQueue Matthias Volk 2018-11-23 13:09:36 +0100
  • d062e658e0 Output progress for DFT exploration Matthias Volk 2018-11-22 13:22:44 +0100
  • 1d683acbde Added assertion Matthias Volk 2018-11-22 11:08:19 +0100
  • 1140d96ba5 Added well-formedness check for DFTs Matthias Volk 2018-11-22 11:08:07 +0100
  • 9376de26c9 Fixed typo Matthias Volk 2018-11-22 11:07:25 +0100
  • 7d9cea09c0 Model Erlang distribution by BEs for each phase and SEQ gate Matthias Volk 2018-11-21 16:51:50 +0100
  • 7adab86f8e Extended Galileo parser to throw exception for inspections Matthias Volk 2018-11-20 18:16:16 +0100
  • 9cb53298fa Extended Galileo parser to support parsing of Erlang distributions Matthias Volk 2018-11-20 17:39:32 +0100
  • 7b1d7507c4 simplified a constructor for assignments for simpler code Sebastian Junges 2018-11-20 22:55:54 +0100
  • b945b34457 extended the subsystembuilder with an option to track actions, and the option to disable some features Sebastian Junges 2018-11-20 22:55:20 +0100
  • c4e7fdd5e5 alternative memoryless scheduler application Sebastian Junges 2018-11-20 22:54:37 +0100
  • 7439b66d71 jani origins, implemented missing compute identifier infos Sebastian Junges 2018-11-05 15:24:01 +0100
  • 82f5b05e90 edge to string method (simplifies some other code fragments), and write color to the string Sebastian Junges 2018-11-05 15:22:58 +0100
  • 595afcfc0a more precise error message when creating non-deterministic models Sebastian Junges 2018-11-05 15:21:39 +0100
  • 7e61ab4a0f Travis: Disable deployment if no credentials are given Matthias Volk 2018-11-20 17:31:58 +0100
  • 14e22dc942 Travis: Better output for build type checks Matthias Volk 2018-11-20 17:31:35 +0100
  • 45cb2b4118 Better debug message in JsonParser Matthias Volk 2018-11-19 00:02:36 +0100
  • c9c2ed09ad Travis: do not deploy for pull requests Matthias Volk 2018-11-18 23:47:19 +0100
  • 6d05ce4c7b Travis: Fixed syntax Matthias Volk 2018-11-18 23:40:42 +0100
  • a2fbcf111b Travis: check build types Matthias Volk 2018-11-16 19:40:18 +0100
  • 1457c60e4b Crucial fix to enable release mode again Matthias Volk 2018-11-16 18:43:03 +0100
  • f6faf9e3a5 Flag for printing information about model generated from DFT Matthias Volk 2018-11-15 18:06:30 +0100
  • 43d1a7d2e9 Added checks for well-formedness of DFT Matthias Volk 2018-11-15 17:41:46 +0100
  • c7d2db4260 Updated extendSpareModule() Matthias Volk 2018-11-15 15:29:21 +0100
  • 5c13fe624f Fixed JSON parser Matthias Volk 2018-11-15 14:15:43 +0100
  • d9d29eeea4 More detailed DFT statistics Matthias Volk 2018-11-15 13:51:40 +0100
  • 909c035c52 Dot export can insert linebreaks between labels Matthias Volk 2018-11-15 11:09:53 +0100
  • d4f4961eb0 Merge branch 'master' Matthias Volk 2018-11-15 10:30:48 +0100
  • 9656d2c253 Supporting export of generated Markov chain from DFT Matthias Volk 2018-11-14 18:11:57 +0100
  • 208ee76edb storm-pars: Added possibility to compute the extremal value within a given region using parameter lifting. TimQu 2018-11-14 16:40:55 +0100
  • b5f37cb8eb Fixed json export for pdep Matthias Volk 2018-11-14 09:46:58 +0100
  • 6444bc7c5e Better error message Matthias Volk 2018-11-13 15:56:00 +0100
  • 7697254635 Fixed computation of dormancy factor for lambda=0 Matthias Volk 2018-11-13 14:42:24 +0100
  • 463f873c04 Fixed json export for restrictions and dependencies Matthias Volk 2018-11-13 14:33:14 +0100
  • f5ad8398db Allow to add properties to a PGCL program. TimQu 2018-11-12 14:27:40 +0100
  • ece2a93f37 Fixed a warning TimQu 2018-11-12 14:27:08 +0100
  • c622f463ad JaniNextStateGenerator: Fixed an issue related to CTMCs without state-action rewards TimQu 2018-11-09 16:36:14 +0100
  • 425eb4b1a9 Made version check for master14 branch of carl more robust Matthias Volk 2018-11-07 13:13:04 +0100
  • d94e1ca275 Fixed warning Matthias Volk 2018-11-07 09:47:33 +0100
  • 9ef0c07db5 Removed unused variable Matthias Volk 2018-11-07 09:39:33 +0100
  • 6fcebed10e More robust handling of BE arguments in Galileo format Matthias Volk 2018-11-04 23:01:02 +0100
  • c0a51c6704 Better error message in GalileoParser Matthias Volk 2018-11-04 19:59:24 +0100
  • a15a0072de Better debug output Matthias Volk 2018-10-30 15:52:55 +0100
  • 106508fcac Fixed adding of DerivedOperators Matthias Volk 2018-10-30 13:53:47 +0100
  • d6d2d96a92 Added JaniExportSettings to storm-dft Matthias Volk 2018-10-30 13:52:47 +0100
  • 55eab08ed5 Allow non constant derivatives in monotonicity analysis Jip Spel 2018-10-30 10:49:58 +0100
  • cb2b01b7ee Fixed compile issue Matthias Volk 2018-10-30 10:09:07 +0100
  • 5a05a2ac33 Merge remote-tracking branch 'origin/master' into storm-pars-analysis-monotonicity Jip Spel 2018-10-29 13:35:44 +0100
  • 748098e891 Output to results.txt file Jip Spel 2018-10-29 13:35:07 +0100
  • d9dbf8706b Merge branch 'master' into dft_gspn_new Matthias Volk 2018-10-29 12:40:22 +0100
  • bd02460aef Merge from master Matthias Volk 2018-10-29 12:40:05 +0100
  • ca3b878654 do not add rate 0 edges to jani (but print a warning) Sebastian Junges 2018-10-29 12:38:59 +0100
  • b04a853319 Check on number of set bits instead of vector size Jip Spel 2018-10-29 12:33:41 +0100
  • 43688d09ea reward infinity scheduler extraction is now correct Sebastian Junges 2018-10-29 11:32:48 +0100
  • af23545a7b Clean up Lattice Extender Jip Spel 2018-10-29 10:27:22 +0100
  • dd1540b4c6 Update lattice Jip Spel 2018-10-29 09:19:11 +0100
  • 93ca559c83 additional sanity checks for scheduler extraction Sebastian Junges 2018-10-28 17:45:39 +0100
  • 7563d168e4 Make sure statesAbove/Below are set correctly Jip Spel 2018-10-26 18:18:37 +0200
  • ae7d334171 Extend test Jip Spel 2018-10-26 18:14:45 +0200
  • 9efea2969b Change implementation of Lattice Jip Spel 2018-10-26 16:16:31 +0200
  • 6b09411122 Fixed an error in the jani location expander. TimQu 2018-10-26 16:11:17 +0200
  • b3987b178c Explicit model builder: Give an error if no initial state is found. TimQu 2018-10-26 16:09:27 +0200
  • e0cc7525b5 Extend Lattice Test Jip Spel 2018-10-26 16:09:23 +0200
  • 9fa297b2aa Fix test Jip Spel 2018-10-26 15:05:01 +0200
  • 78e5108e42 Extend Lattice test Jip Spel 2018-10-26 14:28:32 +0200
  • ca828729ff Fixed a few warnings TimQu 2018-10-26 12:50:10 +0200
  • 602d18d844 Fixed parsing of edge assignments. TimQu 2018-10-26 12:11:19 +0200
  • 16d7dccb4e I am utterly stupid. Fixed an assertion that I changed yesterday Sebastian Junges 2018-10-26 10:50:22 +0200
  • 5d0ec15ad4 clarified error message, as the reward models are present (according to output) but simply empty Sebastian Junges 2018-10-25 20:16:40 +0200
  • 07588df137 operators to remove bounds / optimality types from a formula Sebastian Junges 2018-10-25 19:12:17 +0200
  • 9a0794fca1 refined error message wrt unexpected type of scheduler Sebastian Junges 2018-10-25 19:11:27 +0200
  • f601405d55 set edge color default to zero Sebastian Junges 2018-10-11 10:20:49 +0200
  • 9be488b969 Enabling expected time queries for ctmcs in the hybrid engine. TimQu 2018-10-25 14:48:21 +0200
  • 003922a9e4 Fixed optimization direction when exporting standard petri net properties to jani TimQu 2018-10-25 14:25:33 +0200
  • c27b8af90f Display the time required for parsing the prism/jani input TimQu 2018-10-25 13:47:24 +0200
  • 7038858379 storm-conv: Added ability to make global variables of a jani model local (or vice versa) TimQu 2018-10-24 18:08:08 +0200
  • e6fc962e5e In exact mode, use LP as LRA Method for nondeterministic models. TimQu 2018-10-23 17:07:47 +0200
  • f0f74d1d0a Make use of provided methods when extending the lattice Jip Spel 2018-10-24 14:08:42 +0200
  • 8adac3a897 Merge remote-tracking branch 'origin/master' into storm-pars-analysis-monotonicity Jip Spel 2018-10-24 13:04:34 +0200
  • 728af9526b Change Lattice implementation Jip Spel 2018-10-24 13:00:31 +0200
  • 954eb1f925 Comment out file creation, add precision check in difference between two samples Jip Spel 2018-10-24 13:00:13 +0200
  • b0551b540a Add message if nothing about monotonicity is known Jip Spel 2018-10-22 09:45:48 +0200
  • e94b37d2f5 instantaneous reward properties for continuous time models can not be handled in exact mode. TimQu 2018-10-17 18:32:49 +0200
  • cff6fdd8c6 nix-scripts: Update scripts and add documentation Michael Raitza 2018-10-02 16:16:24 +0200
  • c91005534c nix-scripts: storm -> 02.10.2018 Michael Raitza 2018-10-02 15:53:43 +0200
  • 88e24fb981 nix-scripts: carl 17.12 -> 18.06 Michael Raitza 2018-10-02 15:03:34 +0200
  • 7205e46c80 Add Nix overlay that builds storm and its dependencies Michael Raitza 2018-10-02 14:06:21 +0200
  • fbb355eadb Keep assumptions when both assumptions can not be validated and there is some monotonicity Jip Spel 2018-10-16 11:51:59 +0200
  • 29e22f6de3 Jani JSONExporter: Fixed export of reward accumulation. TimQu 2018-10-16 11:36:14 +0200
  • bbe9253777 JaniParser: Actually fixed parsing of long run average reward formulas TimQu 2018-10-15 16:19:00 +0200
  • 082d624174 Jani: import/export of steady-state properties TimQu 2018-10-15 13:53:19 +0200
  • d9279a72ab Fixed an issue where jani formulas using conjunctions of boolean transient variables could not be parsed. TimQu 2018-10-12 15:12:18 +0200
  • fbdce446b3 Fix SMT validation of assumptions Jip Spel 2018-10-11 16:12:03 +0200
  • 6b216d7fd6 Add additional testsituation Jip Spel 2018-10-11 16:09:14 +0200
  • aba1856786 JaniParser: fixed an issue related to using constants in the definition of other constants. TimQu 2018-10-11 16:05:20 +0200
  • 0434d9f83a fixed issue when checking whether transition rewards can be lifted TimQu 2018-10-11 15:12:44 +0200