Commit Graph

315 Commits

Author SHA1 Message Date
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
Artur Meski
c686317e16 Use enc_state_with_blocking() for HSR 2016-03-03 12:32:14 +01:00
Artur Meski
7907c0216b Added the enc_state_with_blocking() function
This allows to specify reactants and inhibitors in the provided state.
2016-03-03 12:31:12 +01:00
Artur Meski
a869ed25cb remove __pycache__ 2016-03-03 09:25:34 +01:00
Artur Meski
975c01edea Heat Shock Response 2016-03-03 09:22:33 +01:00
Artur Meski
063e8063cc Moved "Next level?" to after we check max_level 2016-03-03 06:54:41 +01:00
Artur Meski
1746bf86c8 still trying with glucose assimilation... 2016-03-02 22:12:50 +01:00
Artur Meski
561413b79f expire_sugar entity 2016-03-02 18:18:36 +01:00
Artur Meski
e879740162 Removal of the log files. 2016-03-02 18:10:47 +01:00
Artur Meski
02606e32bf Permanency encoding. Allows preserving concentration levels for a specified entity. Permanency can also be inhibited. 2016-03-02 18:09:07 +01:00
Artur Meski
6ab5304628 Permanent entities implementation. Allows for preserving concentration levels when the inhibitors are not provided. 2016-03-02 18:08:07 +01:00
Artur Meski
3f3690c861 working on Blood-Glucose example 2016-03-01 21:25:34 +01:00
Artur Meski
0137a20867 simplify 2016-02-29 08:35:49 +01:00
Artur Meski
249e8ca594 Just to be sure... 2016-02-28 22:57:37 +01:00
Artur Meski
ef6f2edd33 Incrementation & decrementation by a specified value. 2016-02-28 20:12:43 +01:00