Artur Meski
|
672e43abce
|
Merge branch 'distrib_rs' of bitbucket.org:rsmodecking/rsmc into distrib_rs
|
2018-10-14 16:16:43 +01:00 |
|
Artur Meski
|
f20fce6c15
|
Merge branch 'distrib_rs' of bitbucket.org:rsmodecking/rsmc into distrib_rs
|
2018-10-14 16:15:44 +01:00 |
|
Artur Meski
|
b3d58504b4
|
TGC generator (with controller as context automaton)
|
2018-10-14 16:15:34 +01:00 |
|
Artur Meski
|
24f783c6a8
|
TGC generator (with controller as context automaton)
|
2018-10-14 16:14:44 +01:00 |
|
Artur Meski
|
a976813c48
|
TGC
|
2018-10-13 22:04:58 +01:00 |
|
Artur Meski
|
e098bcb42b
|
use_ -> make_
|
2018-10-13 21:03:27 +01:00 |
|
Artur Meski
|
e4ab5999aa
|
Make Progressive as option
|
2018-10-13 21:00:06 +01:00 |
|
Artur Meski
|
96b0278136
|
Progressive eca construction
|
2018-10-08 21:01:39 +01:00 |
|
Artur Meski
|
9dc03f8abc
|
Fixed nullptr deref when there is no state constraint
|
2018-10-07 21:56:48 +01:00 |
|
Artur Meski
|
469ca7e46b
|
Added encoding of the DRS state constraints to the context automaton
|
2018-10-07 21:45:28 +01:00 |
|
Artur Meski
|
ac97db8ead
|
Printing of the state constraints in the context automaton
|
2018-09-23 13:12:33 +01:00 |
|
Artur Meski
|
206996a700
|
Building of stateconstr.o; prelim. methods for ctx and state BDD enc.
|
2018-09-22 22:55:00 +01:00 |
|
Artur Meski
|
a36ed9651f
|
Includes, clean-up
We are trying to avoid including stuff whenever possible.
Forward declarations are prefered in most cases, just in case...
|
2018-09-22 20:05:35 +01:00 |
|
Artur Meski
|
d4ac425963
|
state constraints
|
2018-09-22 20:05:19 +01:00 |
|
Artur Meski
|
07171c6d60
|
Optimisations
|
2018-07-22 20:20:14 +01:00 |
|
Artur Meski
|
18e840ce17
|
Partitioned trnasition relation with reordering
|
2018-07-22 18:25:19 +01:00 |
|
Artur Meski
|
482828a04e
|
Benchmarks
|
2018-07-22 15:11:52 +01:00 |
|
Artur Meski
|
41b609326a
|
Benchmarks
|
2018-07-22 15:08:50 +01:00 |
|
Artur Meski
|
f3a6fc6949
|
Benchmarking script
|
2018-07-22 14:17:26 +01:00 |
|
Artur Meski
|
5edab04266
|
Benchmarks
|
2018-07-22 14:12:14 +01:00 |
|
Artur Meski
|
36b5e7b741
|
TGC generator
|
2018-07-17 20:31:26 +01:00 |
|
Artur Meski
|
b0d69d0aa7
|
Property selection
|
2018-07-17 20:26:05 +01:00 |
|
Artur Meski
|
eb2e4e5526
|
Property name
|
2018-07-17 20:10:18 +01:00 |
|
Artur Meski
|
2aefa98aef
|
Identifier
|
2018-07-17 20:04:11 +01:00 |
|
Artur Meski
|
141c25386d
|
ReactICS
|
2018-07-17 19:35:39 +01:00 |
|
Artur Meski
|
964fb71d02
|
Mutex generator (tgc)
|
2018-06-20 17:50:44 +01:00 |
|
Artur Meski
|
54ee79b6b3
|
Changes to the transition relation
|
2018-05-28 18:18:37 +01:00 |
|
Artur Meski
|
1590dacdcb
|
Check for incorrect property number
|
2018-04-29 19:59:02 +01:00 |
|
Artur Meski
|
b7c4cd6906
|
Scalable formula
|
2018-04-29 19:58:17 +01:00 |
|
Artur Meski
|
2aadb9df33
|
Cleanup
|
2018-04-29 18:54:56 +01:00 |
|
Artur Meski
|
06a28f9e54
|
Mutext DRS generator
|
2018-04-29 18:54:19 +01:00 |
|
Artur Meski
|
36b59b5baf
|
Universal K support
|
2018-04-29 17:16:25 +01:00 |
|
Artur Meski
|
142846b90c
|
Fixed a bug with missing process enabledness encoding in context; fixed bit count for CA
|
2018-04-23 20:15:46 +01:00 |
|
Artur Meski
|
3157bb09ef
|
Support for NK
|
2018-04-21 22:26:42 +01:00 |
|
Artur Meski
|
d2a9b5733c
|
RSCTL -> RSCTLK
|
2018-04-21 19:33:32 +01:00 |
|
Artur Meski
|
09578a075f
|
Quantification for only the i-th process
|
2018-04-21 19:15:06 +01:00 |
|
Artur Meski
|
f5e0beb513
|
Parsing of K
|
2018-04-15 20:00:05 +01:00 |
|
Artur Meski
|
81e9d13ade
|
Expistemic operators, quantification
|
2018-04-15 19:01:30 +01:00 |
|
Artur Meski
|
8a9ba95fed
|
Quantification BDDs for each process; example
|
2018-04-15 18:47:52 +01:00 |
|
Artur Meski
|
d34e3954c4
|
First working version of rsCTL verification.
|
2018-04-15 13:20:07 +01:00 |
|
Artur Meski
|
c4c3af0300
|
Removed action sets in formulae
|
2018-04-15 12:25:57 +01:00 |
|
Artur Meski
|
30b62c88c6
|
rsCTL PVs: process_name.entity_name.
|
2018-04-14 22:10:56 +01:00 |
|
Artur Meski
|
cdd463d552
|
Average results
|
2018-04-07 20:52:51 +01:00 |
|
Artur Meski
|
d8398085aa
|
Clean-up
|
2018-04-03 20:37:38 +01:00 |
|
Artur Meski
|
6e54380f14
|
It works!
|
2018-04-03 20:35:12 +01:00 |
|
Artur Meski
|
95d8123a6b
|
Working DRS with one process
|
2018-04-03 20:05:50 +01:00 |
|
Artur Meski
|
5f578c9066
|
Context encoding and complementation
|
2018-04-03 17:50:23 +01:00 |
|
Artur Meski
|
6b485e4e08
|
Transition relation for DRS
|
2018-04-03 17:19:23 +01:00 |
|
Artur Meski
|
9a8255a355
|
Encoding DRS transition relation
|
2018-04-02 22:17:47 +01:00 |
|
Artur Meski
|
f73ebdd4bf
|
BDD initialisation
|
2018-04-02 14:44:44 +01:00 |
|