Commit Graph

79 Commits

Author SHA1 Message Date
Artur Meski
821df2e152 cleanup 2017-03-02 20:59:34 +01:00
Artur Meski
2abf76ae72 logics module 2017-03-02 20:59:07 +01:00
Artur Meski
68c824e2f1 Parameters for rsLTL 2017-03-01 21:08:41 +01:00
Artur Meski
bae7611606 Renaming FormulaLTL -> Formula_rsLTL 2017-02-26 22:27:49 +01:00
Artur Meski
d065dbac83 Renaming FormulaLTL -> Formula_rsLTL 2017-02-26 22:27:29 +01:00
Artur Meski
4e7d640e2f Bag descriptions; oper. overloading for FormLTL and BagDescription 2017-02-26 22:23:06 +01:00
Artur Meski
ac389b238b working on smt encoding for NA 2017-01-01 18:23:02 +01:00
Artur Meski
1594659509 getters for the used actions, automata supporting actions, transitions for actions, etc. 2017-01-01 00:34:27 +01:00
Artur Meski
ebee3aa03e working on RSNA 2016-12-29 20:21:56 +01:00
Artur Meski
ba8cb798e4 clean and cleanall 2016-12-29 20:15:11 +01:00
Artur Meski
be8b434804 rsna 2016-12-29 10:42:27 +01:00
Artur Meski
f367c5d72c network of automata 2016-12-28 22:43:26 +01:00
Artur Meski
58f06c3fc1 cleanup 2016-12-28 22:30:00 +01:00
Artur Meski
bd06d575f7 SmtChecker class moved to legacy 2016-12-28 22:15:40 +01:00
Artur Meski
5e8417baf2 SmtCheckerPGRS -> ..RS; new: SmtCheckerRSNA 2016-12-28 22:13:16 +01:00
Artur Meski
5ddc549245 adding support for network of automata... 2016-12-28 21:36:49 +01:00
Artur Meski
a1b660abea distributed reaction system 2016-12-28 20:59:45 +01:00
Artur Meski
f73d0784ca working on ECA 2016-12-28 18:32:32 +01:00
Artur Meski
b2fa911a77 cleanup 2016-12-28 16:16:24 +01:00
Artur Meski
3d8f4b0958 version date update 2016-12-28 16:10:42 +01:00
Artur Meski
bb87eab5bd cleanup 2016-12-28 16:09:20 +01:00
Artur Meski
1a1bfa6677 cleanup 2016-12-28 15:58:41 +01:00
Artur Meski
c37ca14a22 release UCNC 2016-12-28 15:56:55 +01:00
Artur Meski
e62638fd7b updated imports 2016-12-28 15:55:30 +01:00
Artur Meski
daadf33d02 smt package 2016-12-28 15:55:03 +01:00
Artur Meski
41846b66da rs package 2016-12-28 15:51:59 +01:00
Artur Meski
d5f3f06743 ExtendedContextAutomaton 2016-12-27 22:11:22 +01:00
Artur Meski
56218a3596 some cleanup 2016-12-27 20:57:02 +01:00
Artur Meski
11a2d2ae46 imports 2016-12-27 19:45:07 +01:00
Artur Meski
be3e506cbe ltl formulae 2016-12-18 18:08:21 +01:00
Artur Meski
7dfc02f613 some log files 2016-09-24 15:50:55 +02:00
Artur Meski
f4528fb287 finalised version used for UCNC2016 experiments 2016-03-22 21:34:37 +01:00
Artur Meski
586e085a80 cleanup: examples 2016-03-22 21:33:04 +01:00
Artur Meski
3780be1fa4 Brought back 'dec' entity 2016-03-10 15:00:35 +01:00
Artur Meski
270c0c86ed get_max_concentration_level function 2016-03-10 15:00:28 +01:00
Artur Meski
b71e749c53 Meta reactions are enabled only if no ordinary reaction is 2016-03-10 14:59:48 +01:00
Artur Meski
a0e4dc9fe1 Minor changes to the experiments. Changed the .sh cases to be verified (only even values). 2016-03-10 12:37:23 +01:00
Artur Meski
781777ac56 Production of the maximal concentration
When multiple reactions are enabled, we produce the maximal concentration by exploiting the fact that reactions are sorted (increasing order).  We build the encoding starting from the inner-most reaction (with the lowest concentration level), and then build around that reaction encoding for the reactions with higher concentration levels. This allows us to avoid the disjunctions of possible resulting concentractions. E.g. (x==1 v x==3 v x==7), while we should have only x==7.
2016-03-10 12:33:32 +01:00
Artur Meski
a6aa5e4590 Sorting reactions in the increasing order
(per produced entity's concentration level)
2016-03-10 12:30:14 +01:00
Artur Meski
2387e8ad26 Minor modifications 2016-03-07 21:29:02 +01:00
Artur Meski
3a6d771f04 cosmetics... again :) 2016-03-05 00:08:32 +01:00
Artur Meski
7b2f29c9ec Reachability testing with properties specified with required and blocking entities.
Required entitied correspond to reactants, while blocking entities to inhibitors.
This functionality replaces 'exact' state encoding.
2016-03-04 23:51:53 +01:00
Artur Meski
9f3af0b48c HSR. Translation of properties RSC->RS. Testing with RS and RSC (cmdline args). 2016-03-04 23:50:38 +01:00
Artur Meski
ef1b769654 Translation for permanency (RSC -> RS) 2016-03-04 23:48:28 +01:00
Artur Meski
5d65b4fac2 Added colour.py file 2016-03-04 20:52:30 +01:00
Artur Meski
dc482781e2 Output cosmetics 2016-03-04 20:52:02 +01:00
Artur Meski
45b6db12c4 Pretty printing 2016-03-04 15:10:10 +01:00
Artur Meski
5aec7d8df5 HSR + cosmetics 2016-03-03 16:11:09 +01:00
Artur Meski
ec8e5d1b7d Fixed permanency encoding: And->Or. 2016-03-03 14:35:47 +01:00
Artur Meski
a2d4912d2e cleanup 2016-03-03 12:39:28 +01:00