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

Everybody knows

Browse Source
This commit is contained in:
Artur Meski
2018-11-24 14:23:40 +00:00
parent 34f7b503c1
commit c72eb7ac4a
3 changed files with 29 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
mc.cc
View File

@@ -359,6 +359,14 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
auto proc_id = srs->rs->getProcessID(form->getSingleAgent()); auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
return *reach - (statesNK(*reach - getStatesRSCTLK(form->getLeftSF()), proc_id) * *reach); return *reach - (statesNK(*reach - getStatesRSCTLK(form->getLeftSF()), proc_id) * *reach);
} }
else if (oper == RSCTLK_NE) {
auto proc_set = form->getAgentsAsProcSet(srs->rs);
return statesNE(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_set) * *reach;
}
else if (oper == RSCTLK_UE) {
auto proc_set = form->getAgentsAsProcSet(srs->rs);
return *reach - (statesNE(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
}
else if (oper == RSCTLK_NC) else if (oper == RSCTLK_NC)
{ {
auto proc_set = form->getAgentsAsProcSet(srs->rs); auto proc_set = form->getAgentsAsProcSet(srs->rs);
@@ -463,6 +471,18 @@ BDD ModelChecker::statesNK(const BDD &states, Process proc_id)
return x; return x;
} }
BDD ModelChecker::statesNE(const BDD &states, ProcSet processes)
{
BDD x = BDD_FALSE;
for (auto const &proc_id : processes)
{
x += states.ExistAbstract(getIthOnly(proc_id));
}
return x;
}
BDD ModelChecker::statesNC(const BDD &states, ProcSet processes) BDD ModelChecker::statesNC(const BDD &states, ProcSet processes)
{ {
BDD x = BDD_FALSE; BDD x = BDD_FALSE;

1
mc.hh
View File

@@ -61,6 +61,7 @@ class ModelChecker
BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB); BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB);
BDD statesEFctx(const BDD *contexts, const BDD &states); BDD statesEFctx(const BDD *contexts, const BDD &states);
BDD statesNK(const BDD &states, Process proc_id); BDD statesNK(const BDD &states, Process proc_id);
BDD statesNE(const BDD &states, ProcSet processes);
BDD statesNC(const BDD &states, ProcSet processes); BDD statesNC(const BDD &states, ProcSet processes);
BDD getIthOnly(Process proc_id); BDD getIthOnly(Process proc_id);

8
rsin_parser.yy
View File

@@ -409,6 +409,14 @@ rsctlk_form:
$$ = new FormRSCTLK(RSCTLK_NE, *$3, $6); $$ = new FormRSCTLK(RSCTLK_NE, *$3, $6);
free($3); free($3);
} }
| UC LSB agents RSB LRB rsctlk_form RRB {
$$ = new FormRSCTLK(RSCTLK_UC, *$3, $6);
free($3);
}
| NC LSB agents RSB LRB rsctlk_form RRB {
$$ = new FormRSCTLK(RSCTLK_NC, *$3, $6);
free($3);
}
// | E LSB actions RSB X rsctlk_form { // | E LSB actions RSB X rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6); // $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);