From 3157bb09efdeb3396308b02e33fb4e8d6ba38ad5 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sat, 21 Apr 2018 22:26:42 +0100 Subject: [PATCH] Support for NK --- formrsctlk.cc | 6 ++++++ formrsctlk.hh | 9 +++++++++ in/hsr_drs.rs | 14 +++++++------- mc.cc | 14 ++++++++++++++ mc.hh | 1 + rsin_parser.ll | 4 +++- rsin_parser.yy | 6 ++++++ 7 files changed, 46 insertions(+), 8 deletions(-) diff --git a/formrsctlk.cc b/formrsctlk.cc index 5870709..334fa0d 100644 --- a/formrsctlk.cc +++ b/formrsctlk.cc @@ -151,6 +151,12 @@ std::string FormRSCTLK::toStr(void) const else if (oper == RSCTLK_AF_ACT) { return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")"; } + else if (oper == RSCTLK_NK) { + return "NK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTLK_UK) { + return "UK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")"; + } else { return "??"; diff --git a/formrsctlk.hh b/formrsctlk.hh index 008e5a1..b992ff6 100644 --- a/formrsctlk.hh +++ b/formrsctlk.hh @@ -372,6 +372,15 @@ class FormRSCTLK } } bool isERSCTLK(void) const; + Agents_f getAgents(void) const + { + return agents; + } + std::string getSingleAgent(void) const + { + assert(oper == RSCTLK_NK || oper == RSCTLK_UK); + return *(agents.begin()); + } }; #endif diff --git a/in/hsr_drs.rs b/in/hsr_drs.rs index f4bcd00..51c33af 100644 --- a/in/hsr_drs.rs +++ b/in/hsr_drs.rs @@ -44,21 +44,21 @@ context-automaton { } # P1 -rsctl-property { AG(mainA.hse OR mainA.hsf3:hse IMPLIES AX(mainA.hse OR mainA.hsf3:hse)) } +rsctlk-property { AG(mainA.hse OR mainA.hsf3:hse IMPLIES AX(mainA.hse OR NK[mainA]( mainA.hsf3:hse ))) } # P2 -#rsctl-property { A[{stress},{nostress}]G(~(hse AND hsf3:hse) IMPLIES A[{stress},{nostress}]X(~(hse AND hsf3:hse))) } +#rsctlk-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)) } +#rsctlk-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)) } +#rsctlk-property { A[{stress},{nostress}]G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) } +#rsctlk-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) ) ) } +#rsctlk-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)) } +#rsctlk-property { A[{nostress}]G(hsp:hsf IMPLIES A[{nostress}]X (hsp:hsf)) } diff --git a/mc.cc b/mc.cc index 0ad65f6..95c82c3 100644 --- a/mc.cc +++ b/mc.cc @@ -346,6 +346,10 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form) return !statesEGctx(form->getActionsBDD(), !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach; } + else if (oper == RSCTLK_NK) { + auto proc_id = srs->rs->getProcessID(form->getSingleAgent()); + return statesNK(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_id) * *reach; + } assert(0); // Should never happen return BDD_FALSE; @@ -430,6 +434,16 @@ BDD ModelChecker::statesEFctx(const BDD *contexts, const BDD &states) return x; } +BDD ModelChecker::statesNK(const BDD &states, Process proc_id) +{ + // bdd = new BDD((arg[0]->satStates(reach) * reach).ExistAbstract(bddOnlyIth(getAgent())) * reach); + BDD x = states; + + x = x.ExistAbstract(getIthOnly(proc_id)); + + return x; +} + BDD ModelChecker::getIthOnly(Process proc_id) { /* if possible, we return the BDD from cache */ diff --git a/mc.hh b/mc.hh index 9685c47..54b87b9 100644 --- a/mc.hh +++ b/mc.hh @@ -60,6 +60,7 @@ class ModelChecker BDD statesEGctx(const BDD *contexts, const BDD &states); BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB); BDD statesEFctx(const BDD *contexts, const BDD &states); + BDD statesNK(const BDD &states, Process proc_id); BDD getIthOnly(Process proc_id); diff --git a/rsin_parser.ll b/rsin_parser.ll index a946223..3750a72 100644 --- a/rsin_parser.ll +++ b/rsin_parser.ll @@ -68,6 +68,8 @@ blank [ \t] "XOR" return token::XOR; "IMPLIES" return token::IMPLIES; "~" return token::NOT; +"A" return token::A; +"E" return token::E; "EX" return token::EX; "EU" return token::EU; "EF" return token::EF; @@ -83,7 +85,7 @@ blank [ \t] "K" return token::UK; "C" return token::UC; "D" return token::UD; -"E" return token::UE; +"UE" return token::UE; "NK" return token::NK; "NC" return token::NC; "ND" return token::ND; diff --git a/rsin_parser.yy b/rsin_parser.yy index 827eda5..440cc8a 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -370,6 +370,12 @@ rsctlk_form: $$ = new FormRSCTLK(RSCTLK_UK, agents, $6); free($3); } + | NK LSB IDENTIFIER RSB LRB rsctlk_form RRB { + Agents_f agents; + agents.insert(*$3); + $$ = new FormRSCTLK(RSCTLK_NK, agents, $6); + free($3); + } // | E LSB actions RSB X rsctlk_form { // $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);