Commits · 9b20334e7fad4ced85917596e7266690f2502710 · mbe-tools / TTool

May 07, 2020
- First version model-checker validator which validates internal verification results with UPPAAL · 9b20334e
  tempiaa authored 4 years ago
  
  9b20334e
Apr 30, 2020
- Better organization of graphic elements in model-checking window · 6f3c792a
  tempiaa authored 4 years ago
  
  6f3c792a
- Optimized synchronization of signals for better performance · c8134e3a
  tempiaa authored 4 years ago
  
  c8134e3a
Apr 29, 2020
- More expression solver tests · 8a2db960
  tempiaa authored 4 years ago
  
  8a2db960
- Test for Expression Solver plus fixes · 2b471ac8
  tempiaa authored 4 years ago
  
  2b471ac8
Apr 28, 2020
- Updated the documentation for the model-checker, cleaned attributes in SafetyProperty · 18eafdb8
  tempiaa authored 4 years ago
  
  18eafdb8
Apr 27, 2020
- Added tests for model-checker · 2e0589ae
  tempiaa authored 4 years ago
  
  2e0589ae
Apr 24, 2020
- Added non-computation state of property when not already computed · ef6420ba
  tempiaa authored 4 years ago
  
  ef6420ba
- Model-checker: memory heap footprint further reduced · 6add33b4
  tempiaa authored 4 years ago
  
  6add33b4
- Model-checker: improved heap memory footprint of about 60% · 43e030d2
  tempiaa authored 4 years ago
  
  43e030d2
Apr 23, 2020
- Added support to also response pragmas (p-->q), improved the code · 9082ae63
  tempiaa authored 4 years ago
  
  9082ae63
- Expression solver can represent states of the model as variables. Now... · 57790fac
  tempiaa authored 4 years ago
  
  Expression solver can represent states of the model as variables. Now expression solver proves also safaty pragmas on states.
  57790fac
Apr 22, 2020
- Added safety pragmas on states. Generalized liveness check as a safety check · febcc018
  tempiaa authored 4 years ago
  
  febcc018
Apr 21, 2020
- Expression Solver for action on signal. Start developing safety properties on states · cd5beaac
  tempiaa authored 4 years ago
  
  cd5beaac
Apr 20, 2020
- Assigment Action using the new expression evaluator · 0663831b
  tempiaa authored 4 years ago
  
  0663831b
- New guard evaluator, using precomputing and the optimized expression solver... · 4bb94c12
  tempiaa authored 4 years ago
  
  New guard evaluator, using precomputing and the optimized expression solver ~80x speedup in modelchecker
  4bb94c12
- Added a new boolean expression evaluator with a binary tree structure to... · 7eeb3c34
  tempiaa authored 4 years ago
  
  Added a new boolean expression evaluator with a binary tree structure to reduce the high number of String operations. Used for now only on safety
  7eeb3c34
Apr 16, 2020
- Code cleaning · f9cab654
  tempiaa authored 4 years ago
  
  f9cab654
- Fix of a race condition · 93a1ac79
  tempiaa authored 4 years ago
  
  93a1ac79
- Code cleaning · 3e33b344
  tempiaa authored 4 years ago
  
  3e33b344
- First implementation of safety pragmas check · 804a311b
  tempiaa authored 4 years ago
  
  804a311b
Apr 15, 2020
- Continued changes to support safety pragmas · 04021c0d
  tempiaa authored 4 years ago
  
  04021c0d
- Started procedure to add safety pragmas check to the model-checker · 4b340dd9
  tempiaa authored 4 years ago
  
  4b340dd9
Apr 10, 2020
- Added model-checker tests for liveness, reachability and state limit · 0f216ff3
  tempiaa authored 4 years ago
  
  0f216ff3
- Liveness: moved to multithread DFS instead of BFS to limit state explosion and... · d06f7003
  tempiaa authored 4 years ago
  
  Liveness: moved to multithread DFS instead of BFS to limit state explosion and to find in a considerable faster amount of time a counter example (loop or deadlock). Live paths are pruned.
  d06f7003
Apr 09, 2020
- Little speedup to loop check for liveness · c2ed1204
  tempiaa authored 4 years ago
  
  c2ed1204
- Added command line parameters for model-checker options · 0fd4d500
  tempiaa authored 4 years ago
  
  0fd4d500
Apr 07, 2020
- Added alt conditions to stop liveness check when the liveness is verified true... · d27739bd
  tempiaa authored 4 years ago
  
  Added alt conditions to stop liveness check when the liveness is verified true for all the pending paths
  d27739bd
Apr 06, 2020
- From String to StringBuilder · d6d67be0
  tempiaa authored 4 years ago
  
  d6d67be0
- Small fix in avatar model-checker · b67ab930
  tempiaa authored 4 years ago
  
  b67ab930
Apr 03, 2020
- Now multiple liveness and reachability analyses are possible · ea524f78
  tempiaa authored 4 years ago
  
  ea524f78
- Liveness check on the fly for finite state reachability graphs · 9ff2bc92
  tempiaa authored 4 years ago
  
  9ff2bc92
Apr 02, 2020
- Liveness update: liveness check extended to also StateMachineElements and not... · df26eede
  tempiaa authored 4 years ago
  
  Liveness update: liveness check extended to also StateMachineElements and not only StateElements. It supports only one check per time by now
  df26eede
- First implementation of liveness check on one state for finite-states reachability graphs · 8f22b4f1
  tempiaa authored 4 years ago
  
  8f22b4f1
Mar 30, 2020
- Fix in time limit checkbox state · b2347b8f
  tempiaa authored 4 years ago
  
  b2347b8f
Mar 27, 2020
- Implementation of a time limited graph generation · 41604271
  tempiaa authored 4 years ago
  
  41604271
- Added a draft implementation of a time limited graph generation · 03b8c0b8
  tempiaa authored 4 years ago
  
  03b8c0b8
Mar 26, 2020
- few fixes for race conditions · 287c525c
  tempiaa authored 5 years ago
  
  287c525c
- Fix in number of displayed deadlocks when limiting the number of states · e9b4785b
  tempiaa authored 5 years ago
  
  e9b4785b
- BUG: solved in computeAllInternalStatesFrom due to a possible race condition... · 6fa904f2
  tempiaa authored 5 years ago
  
  BUG: solved in computeAllInternalStatesFrom due to a possible race condition between threads that led to a wrong RG
  6fa904f2