Commit Graph

43 Commits

Author SHA1 Message Date
Artur Meski
b0f24e26db Reordering, verbosity 2018-10-20 21:26:01 +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
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
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
54ee79b6b3 Changes to the transition relation 2018-05-28 18:18:37 +01:00
Artur Meski
b7c4cd6906 Scalable formula 2018-04-29 19:58:17 +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
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
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
212321c6cb Parsing, printing... Context in CA 2018-03-29 17:01:28 +01:00
Artur Meski
5f1a759c8f Reformatting 2018-03-28 21:00:44 +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
Artur Meski
1f01dce3cc Formatting, initial state encoding 2018-03-26 22:29:11 +01:00
Artur Meski
03cbf26afa Bugfixes 2018-03-26 22:05:23 +01:00
Artur Meski
76ab891786 Transition relation encoding 2018-03-26 21:37:43 +01:00
Artur Meski
0c9665d1b6 Typo 2018-03-26 19:22:19 +01:00
Artur Meski
e3119099ea Context automaton state encoding 2018-03-26 19:18:41 +01:00
Artur Meski
fa587e6f2a Started on encoding for CA 2018-03-26 13:10:26 +01:00
Artur Meski
ee441ab390 Types 2018-03-26 11:00:23 +01:00
Artur Meski
44ea91c10e Types in separate file. Other stuff... 2018-03-26 10:47:46 +01:00
Artur Meski
600f5c0daa Initial RS states vs initial CA states (they are incompatible) 2018-03-04 19:46:09 +00:00
Artur Meski
c853e40ad7 RS with context automaton (we embed CA with RS) 2018-03-03 21:19:13 +00:00
Artur Meski
f121ce12fd Reaction system initialisation based on options. 2018-02-25 19:47:00 +00:00
Artur Meski
6dbdd586d6 atom -> entity 2018-02-17 17:09:17 +00:00
Artur Meski
69a9825c8b APM: RSMC version 1.0 (not 1.0a) from ipisvn 2017-11-18 20:30:18 +00:00