Commit Graph

351 Commits

Author SHA1 Message Date
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
Artur Meski
a74bc58a0c Initialisation of BDD variables 2018-04-01 20:59:10 +01:00
Artur Meski
04d2b628f5 Maps for local entities 2018-03-30 20:07:24 +01:00
Artur Meski
dc241ebf78 Cleanup 2018-03-30 18:32:34 +01:00
Artur Meski
c89e336862 Printing of entities per proc 2018-03-30 18:30:08 +01:00
Artur Meski
e3ed26e4a1 Entities used per process (in reactions) 2018-03-30 17:51:29 +01:00
Artur Meski
bac84bfe9a Formatting 2018-03-29 17:02:55 +01:00
Artur Meski
212321c6cb Parsing, printing... Context in CA 2018-03-29 17:01:28 +01:00
Artur Meski
38683e1041 Makefile update 2018-03-28 21:02:46 +01:00
Artur Meski
5f1a759c8f Reformatting 2018-03-28 21:00:44 +01:00
Artur Meski
c90a87875a Context automaton with augmented context: parsing 2018-03-28 20:46:19 +01:00
Artur Meski
753b217721 Printing of reactions 2018-03-28 18:58:59 +01:00
Artur Meski
99fbed638c Reactions organised by process 2018-03-28 18:11:00 +01:00
Artur Meski
179c199ece Processes, switching 2018-03-28 15:35:48 +01:00
Artur Meski
91ccf628f5 Example for CA 2018-03-27 18:31:40 +01:00
Artur Meski
ae740fa885 PV vectors for global state with CA, states printing (resolved an issue with duplicates) 2018-03-27 18:19:06 +01:00
Artur Meski
c74d4bdd0c Context automaton works with RS 2018-03-27 15:41:50 +01:00