artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Quantification BDDs for each process; example

Browse Source
This commit is contained in:
Artur Meski
2018-04-15 18:47:52 +01:00
parent d34e3954c4
commit 8a9ba95fed
3 changed files with 72 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

64
in/hsr_drs.rs Normal file
View File

@@ -0,0 +1,64 @@
options { use-context-automaton; }
reactions {
mainA {
{{hsf},{hsp} -> {hsf3}}; #10
{{hsf,hsp,mfp},{dI} -> {hsf3}}; #11
{{hsf3},{hse,hsp} -> {hsf}}; #12
{{hsf3,hsp,mfp},{hse} -> {hsf}}; #13
{{hsf3,hse},{hsp} -> {hsf3:hse}}; #14
{{hsf3,hse,hsp,mfp},{dI} -> {hsf3:hse}}; #15
{{hse},{hsf3} -> {hse}}; #16
{{hse,hsf3,hsp},{mfp} -> {hse}}; #17
{{hsf3:hse},{hsp} -> {hsf3:hse,hsp}}; #18
{{hsf3:hse,hsp,mfp},{dI} -> {hsf3:hse,hsp}}; #19
{{hsp,hsf},{mfp} -> {hsp:hsf}}; #20
{{hsp:hsf,stress},{nostress} -> {hsp,hsf}}; #21
{{hsp:hsf,nostress},{stress} -> {hsp:hsf}}; #22
{{hsp,hsf3},{mfp} -> {hsp:hsf}}; #23
{{hsp,hsf3:hse},{mfp} -> {hsp:hsf,hse}};
{{prot,stress},{nostress} -> {prot,mfp}};
{{prot,nostress},{stress} -> {prot}};
{{hsp,mfp},{dI} -> {hsp:mfp}};
{{mfp},{hsp} -> {mfp}};
{{hsp:mfp},{dI} -> {hsp,prot}};
};
dummy {
{{mfp},{hsp} -> {mfp}};
};
}
context-automaton {
states { s0, s1 }
init-state { s0 }
transitions {
{ mainA={hsf,prot,hse,nostress} }: s0 -> s1;
{ mainA={hsf,prot,hsp:hsf,stress} }: s0 -> s1;
{ mainA={hsp,prot,hsf3:hse,mfp,hsp:mfp,nostress} }: s0 -> s1;
{ mainA={stress} }: s1 -> s1;
{ mainA={nostress} }: s1 -> s1;
{ mainA={stress,nostress} }: s1 -> s1;
}
}
# P1
rsctl-property { A<mainA.stress XOR mainA.nostress>G(mainA.hse OR mainA.hsf3:hse IMPLIES A<mainA.stress XOR mainA.nostress>X(mainA.hse OR mainA.hsf3:hse)) }
# P2
#rsctl-property { A[{stress},{nostress}]G(~(hse AND hsf3:hse) IMPLIES A[{stress},{nostress}]X(~(hse AND hsf3:hse))) }
# P3
#rsctl-property { A[{stress},{nostress}]G(prot IMPLIES A[{stress},{nostress}]X(prot)) }
# P4
#rsctl-property { A[{stress},{nostress}]G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
#rsctl-property { A< stress XOR nostress >G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
# P5
#rsctl-property { A[{stress},{nostress}]G( ((hsf XOR hsf3 XOR hsf3:hse XOR hsp:hsf) OR ~(hsf OR hsf3 OR hsf3:hse OR hsp:hsf)) IMPLIES A[{stress},{nostress}]X( (hsf XOR hsf3 XOR hsf3:hse XOR hsp:hsf) OR ~(hsf OR hsf3 OR hsf3:hse OR hsp:hsf) ) ) }
# P6
#rsctl-property { A[{nostress}]G(hsp:hsf IMPLIES A[{nostress}]X (hsp:hsf)) }

6
symrs.cc
View File

@@ -118,6 +118,8 @@ void SymRS::initBDDvars(void)
pv_drs_flat = new BDDvec(totalRctSysStateVars);
pv_drs_flat_succ = new BDDvec(totalRctSysStateVars);
pv_drs_E = new BDDvec(numberOfProc);
pv_drs_flat_E = new BDD(BDD_TRUE);
pv_drs_flat_succ_E = new BDD(BDD_TRUE);
@@ -151,6 +153,8 @@ void SymRS::initBDDvars(void)
(*pv_drs)[proc_id].resize(entities_count);
(*pv_drs_succ)[proc_id].resize(entities_count);
(*pv_drs_E)[proc_id] = BDD_TRUE;
for (unsigned int i = 0; i < entities_count; ++i) {
assert(drs_flat_index < totalRctSysStateVars);
@@ -162,6 +166,8 @@ void SymRS::initBDDvars(void)
(*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
(*pv_drs_succ)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
(*pv_drs_E)[proc_id] *= (*pv_drs)[proc_id][i];
// The DRS part of the system (flattened): these vars do not include CA
(*pv_drs_flat)[drs_flat_index] = (*pv_drs)[proc_id][i];
(*pv_drs_flat_succ)[drs_flat_index] = (*pv_drs_succ)[proc_id][i];

2
symrs.hh
View File

@@ -216,6 +216,8 @@ class SymRS
(per DRS process) */
vector<BDDvec> *pv_drs_succ; /*!< PVs for the product (successor)
part of state (per DRS process) */
BDDvec *pv_drs_E; /*!< Quantification BDDs for each process */
BDDvec *pv_drs_flat; /*!< PVs for the DRS product part of state (flat) */
BDDvec *pv_drs_flat_succ; /*!< PVs for the DRS product (successor) part of state (flat) */