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

Commit Graph

  • adaba03648 ExpressionManager: Asserted that when getting a variable with declareOrGetVariable, the returned type is as expected. Tim Quatmann 2019-04-29 09:25:50 +0200
  • c068b7e387 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-04-29 08:57:13 +0200
  • 160c6a67f4 Added missing method in case z3 lp solver is not available. Tim Quatmann 2019-04-29 07:24:30 +0200
  • 4322d00034 FilteredRewardModel: added create method that works without a checkout. Tim Quatmann 2019-04-29 07:24:09 +0200
  • ee090b630e deterministic schedulers: Refactored code for lp-based checker. Tim Quatmann 2019-04-29 07:21:22 +0200
  • c72b97dfca Cleared unused variable warning. TimQu 2019-04-26 15:58:54 +0200
  • 76cabb8287 geometry: Fixed a merge issue. TimQu 2019-04-26 12:18:42 +0200
  • 886bead969 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-04-25 17:27:28 +0200
  • cf25f2f941 SparseMatrix: Create a pretty string of the matrix dimensions. Tim Quatmann 2019-04-25 17:24:01 +0200
  • 138e0f2cee solver: Implemented incremental support for LP solvers (Z3 and Gurobi) Tim Quatmann 2019-04-25 17:23:37 +0200
  • 1eee9a89bd storage/geometry/polytopes: New Methods: setminus and clean Tim Quatmann 2019-04-25 17:22:46 +0200
  • 3a21ce8009 utility/vector: buildVectorForRange now gets the type of the vector as a template parameter. Tim Quatmann 2019-04-25 17:22:09 +0200
  • 0f0a586230 First version of MILP based deterministic scheduler technique. Tim Quatmann 2019-04-25 17:09:06 +0200
  • f16b488590 Added conservative lower bound correction Alexander Bork 2019-04-25 17:06:47 +0200
  • a669c69fc9 Added tests for SMT encoding Alexander Bork 2019-04-25 13:01:08 +0200
  • aff9d21811 Easier fix for bound computation using SMT encoding Alexander Bork 2019-04-25 11:11:21 +0200
  • b89f8f8de4 Refactoring of SMT tests Alexander Bork 2019-04-24 12:55:18 +0200
  • 5d5487140f Fixed bound calculation for SMT encoding Alexander Bork 2019-04-24 12:25:04 +0200
  • f2840f3a66 Explore relevant events further even if the DFT has already failed Matthias Volk 2019-04-23 18:16:14 +0200
  • 944c5ac0fe Only set operational BEs as failable Matthias Volk 2019-04-23 18:15:18 +0200
  • f1c91d9280 Test case for SEQ bug Matthias Volk 2019-04-22 23:27:51 +0200
  • 32dc2dbcc0 Fixed bug where children of SEQ gates were not properly enabled Matthias Volk 2019-04-22 23:18:44 +0200
  • 0f1b05f28c Added support for '_dc' label suffix Matthias Volk 2019-04-18 11:37:42 +0200
  • c272e65d30 Changed suffix label for failed elements to '_failed' Matthias Volk 2019-04-18 11:24:18 +0200
  • 92d05ec368 Fixed handling of relevant events from properties Matthias Volk 2019-04-18 11:11:36 +0200
  • 534d2cf51b Fixed concatenation of multiple properties Matthias Volk 2019-04-18 10:48:44 +0200
  • 0a1ed0270a Output relevant events for better debugging Matthias Volk 2019-04-18 10:48:10 +0200
  • 9398832ce8 Add formula in parse exception for easier debugging Matthias Volk 2019-04-18 10:45:45 +0200
  • b77009897f Ensure unique names in JSON Parser Matthias Volk 2019-04-18 10:05:09 +0200
  • 22c6dfc212 Merge from master Matthias Volk 2019-04-17 22:42:01 +0200
  • 2b8cf84c97 Adapted tests to changes Matthias Volk 2019-04-17 19:19:08 +0200
  • f2c902eedb Set labels, dont care propagation and unique failed state according to relevant events Matthias Volk 2019-04-17 19:11:34 +0200
  • 51959d4334 Set labels in property as relevant events as well Matthias Volk 2019-04-17 18:28:23 +0200
  • ef08ddd2f7 Small refactoring for ElementState Matthias Volk 2019-04-17 17:29:33 +0200
  • 9bf4348677 Test cases for DFT model building with relevant events Matthias Volk 2019-04-17 15:01:50 +0200
  • 10f01f66e2 Ignore relevant events for Don't care propagation Matthias Volk 2019-04-17 14:56:19 +0200
  • 2cf53af750 Proper handling of disabling/enabling events for SEQ and MUTEX Matthias Volk 2019-04-11 17:49:13 +0200
  • 9ce3f9f58d Added tests for mutex Matthias Volk 2019-04-11 11:03:13 +0200
  • 9c226f8336 Added support for MUTEX (but without DC support) Matthias Volk 2019-04-11 11:02:45 +0200
  • 1b8d0a23ed Allow empty choices due to restrictions in state exploration Matthias Volk 2019-04-10 17:51:56 +0200
  • b38b28679f Fixed seqfault when no property was given Matthias Volk 2019-04-10 16:46:36 +0200
  • 7ff1511570 Updated some TODOS Matthias Volk 2019-04-10 16:23:35 +0200
  • 256137b080 Some refactoring Matthias Volk 2019-04-05 19:10:14 +0200
  • 972371c9a2 Started on the notion of 'relevant events' for DFT analysis Matthias Volk 2019-04-05 19:07:48 +0200
  • 8090448564 Some more refactoring Matthias Volk 2019-04-05 16:13:24 +0200
  • 9d81730fe3 Fixed JSON import after changes in BEs Matthias Volk 2019-04-04 17:23:09 +0200
  • 365b7e7673 Removed mChildren in DFTRestriction Matthias Volk 2019-04-04 11:21:24 +0200
  • 723caeb56e Removed mChildren in DFTGate Matthias Volk 2019-04-04 11:04:40 +0200
  • 56636fc4b0 Added missing break statement Matthias Volk 2019-04-04 00:31:43 +0200
  • ed94c79c1a Continue refactoring Matthias Volk 2019-04-04 00:31:29 +0200
  • 10c29d936b Refactoring DFT elements Matthias Volk 2019-04-03 23:17:43 +0200
  • c91033ebb1 Fixed bitshift for DFT isomorphism Matthias Volk 2019-04-03 17:26:32 +0200
  • 3bf14c5198 Larger refactoring for DFT BEs. Split into BEExponential and BEConst Matthias Volk 2019-04-03 17:15:11 +0200
  • 3183a141d6 Started on support for constant failed/failsafe BEs Matthias Volk 2019-03-24 18:06:24 +0100
  • 1f5d3b9479 Correct initialization of priority queue Matthias Volk 2019-03-24 18:05:21 +0100
  • 19ba1c38e7 Set correct order for priorities according to heuristic Matthias Volk 2019-03-22 19:04:01 +0100
  • ef16ba576c Added default case for switch Matthias Volk 2019-03-22 18:58:34 +0100
  • 144fa1c898 Throw exception instead of assertion Matthias Volk 2019-03-22 10:15:37 +0100
  • 6dbe2441b9 Removed unnecessary members Matthias Volk 2019-03-19 16:23:52 +0100
  • 2ebac862e2 Added test cases for DFT approximation Matthias Volk 2019-03-19 14:46:25 +0100
  • 7a8dbf8828 Heuristic is argument for functions in approximation algorithm Matthias Volk 2019-03-19 14:45:30 +0100
  • 5d8fc7db77 Removed approximation heuristic NONE Matthias Volk 2019-03-19 11:28:14 +0100
  • 37d0b66e73 Some fixes for approximation Matthias Volk 2019-03-19 11:14:27 +0100
  • 6eb2795b68 Fixed crucial bug marking all states as 'to expand'. As a result no states were skipped during exploration and no approximation took place. Matthias Volk 2019-03-18 22:40:40 +0100
  • 0904c01828 Make exploration heuristic choosable Matthias Volk 2019-03-18 22:39:39 +0100
  • e53d946b04 Refactored BucketPriorityQueue Matthias Volk 2019-03-18 22:02:36 +0100
  • 6afcaa291d Refactored DftExplorationHeuristic Matthias Volk 2019-03-18 22:01:07 +0100
  • 34edb426be Fixed arguments for exploration heuristic settings Matthias Volk 2019-03-13 14:15:59 +0100
  • 98f3cdbfaf Adapted tests to changes Matthias Volk 2019-04-17 19:19:08 +0200
  • 5952aa8a6f Set labels, dont care propagation and unique failed state according to relevant events Matthias Volk 2019-04-17 19:11:34 +0200
  • d06cf59eba Added SMT function to calculate lower bound for number of DFT failures needed for failure of TLE Alexander Bork 2019-04-17 18:49:08 +0200
  • 4b1af3c51e Set labels in property as relevant events as well Matthias Volk 2019-04-17 18:28:23 +0200
  • d140da92cc Small refactoring for ElementState Matthias Volk 2019-04-17 17:29:33 +0200
  • 58a4491f72 Test cases for DFT model building with relevant events Matthias Volk 2019-04-17 15:01:50 +0200
  • b4f34b13bf Ignore relevant events for Don't care propagation Matthias Volk 2019-04-17 14:56:19 +0200
  • efcff20017 Merge branch 'master' into dftSMT Alexander Bork 2019-04-17 14:14:32 +0200
  • 1976a41298 Reworked solver integration Alexander Bork 2019-04-17 14:07:15 +0200
  • 4507b484d5 Re-added option to export DFTs to smtlib2 SMT files Alexander Bork 2019-04-17 11:34:45 +0200
  • b1278fdece Merge branch 'master' into deterministicScheds Tim Quatmann 2019-04-12 09:13:40 +0200
  • cbbd812b42 Proper handling of disabling/enabling events for SEQ and MUTEX Matthias Volk 2019-04-11 17:49:13 +0200
  • 29b0c4a78f First version of SMT solver integration for DFT analysis Alexander Bork 2019-04-11 16:04:42 +0200
  • eb15177801 cli: try to recover after checking a property has failed. (related to GitHub issue #42) TimQu 2019-04-11 15:13:05 +0200
  • e8003769ca JaniParser: Better error messages for property parsing. TimQu 2019-04-11 15:12:11 +0200
  • e2dc274977 Added export for globally properties in JANI. TimQu 2019-04-11 15:10:52 +0200
  • fc9befbe9e Added toExpression functions for SMT constraints Alexander Bork 2019-04-11 14:22:13 +0200
  • e9119154d7 JaniParser: Fixed parsing of globally formulas in JANI. (GitHub issue #42) TimQu 2019-04-11 14:09:44 +0200
  • 2ccd6d22dc Added tests for mutex Matthias Volk 2019-04-11 11:03:13 +0200
  • d4f56ac724 Added support for MUTEX (but without DC support) Matthias Volk 2019-04-11 11:02:45 +0200
  • 7cab3985c0 Added basis for SMT solver integration Alexander Bork 2019-04-10 18:10:04 +0200
  • ee02357612 Allow empty choices due to restrictions in state exploration Matthias Volk 2019-04-10 17:51:56 +0200
  • 86c183a342 Fixed seqfault when no property was given Matthias Volk 2019-04-10 16:46:36 +0200
  • 01df35236b Updated some TODOS Matthias Volk 2019-04-10 16:23:35 +0200
  • 33b6ba6d8f Refactoring of constraint generation Alexander Bork 2019-04-10 15:20:43 +0200
  • a7a3a82d89 Prism: ToJaniConverters now enforces variables occurring in properties to become global. This fixes GitHub issue #40 TimQu 2019-04-10 13:37:43 +0200
  • 98e0fcd113 jani::Property: Flagged functions of PropertyInterval as const TimQu 2019-04-09 18:53:01 +0200
  • 91b763d218 JaniExporter: Export accumulation for LRA properties correctly. TimQu 2019-04-09 17:35:51 +0200
  • 0d8ecaff35 JaniParser: Transform reward bounds into time- or step bound if appropriate. Added some checks and warnings. TimQu 2019-04-09 17:35:21 +0200
  • a35cb2643a Extend error message Jip Spel 2019-04-09 15:07:16 +0200
  • f2fe674656 JaniParser: made the model available when parsing the property. TimQu 2019-04-09 14:58:22 +0200
  • 8313dc5ef1 Flipped the condition for an exception. TimQu 2019-04-07 15:32:50 +0200