Skip to content
Snippets Groups Projects
Commit 4251f989 authored by Jaime Arias's avatar Jaime Arias
Browse files

refactor: AccessibleEpsilon functions

parent f4918abe
No related branches found
No related tags found
1 merge request!3Full refactoring applying some conventions
Pipeline #9225 passed with stage
......@@ -284,46 +284,40 @@ bdd RdPBDD::ReachableBDD3() const {
return reached;
}
bdd RdPBDD::AccessibleEpsilon2(bdd Init) {
bdd Reached, New, From;
Reached = From = Init;
bdd RdPBDD::AccessibleEpsilon(const bdd &from_s) const {
bdd m1;
bdd m2 = from_s;
do {
bdd succ;
for (Set::const_iterator i = non_observable.begin();
!(i == non_observable.end()); i++)
succ = relation[(*i)](From) | succ;
New = succ - Reached;
From = New;
Reached = Reached | New;
} while (New != bddfalse);
cout << endl;
return Reached;
m1 = m2;
for (const int i : non_observable) {
m2 = relation[i](m2) | m2;
}
} while (m1 != m2);
return m2;
}
bdd RdPBDD::AccessibleEpsilon(bdd from) {
bdd M1;
bdd M2 = from;
// int it=0;
// cout<<"Ici accessible epsilon"<<endl;
bdd RdPBDD::AccessibleEpsilon2(const bdd &from_s) const {
bdd new_bdd;
bdd from = from_s;
bdd reached = from_s;
do {
M1 = M2;
for (Set::const_iterator i = non_observable.begin();
!(i == non_observable.end()); i++) {
// cout<<" unobs : "<<transitions[*i].name<<endl;
bdd succ = relation[(*i)](M2);
M2 = succ | M2;
bdd succ;
for (const int i : non_observable) {
succ = relation[i](from) | succ;
}
// TabMeta[nbmetastate]=M2;
// int intsize=bdd_anodecount(TabMeta,nbmetastate+1);
// if(MaxIntBdd<intsize)
// MaxIntBdd=intsize;
// it++;
// cout << bdd_nodecount(M2) << endl;
} while (M1 != M2);
// cout << endl;
// cout<<"Fin accessible epsilon"<<endl;
return M2;
} /*------------------------ StepForward() --------------*/
new_bdd = succ - reached;
from = new_bdd;
reached = reached | new_bdd;
} while (new_bdd != bddfalse);
return reached;
}
/*------------------------ StepForward() --------------*/
bdd RdPBDD::StepForward2(bdd from) {
// //cout<<"Debut Step Forward \n";
bdd Res;
......
......@@ -68,8 +68,8 @@ class RdPBDD {
bdd ReachableBDD3() const;
// transitive closure on unobserved transitions
bdd AccessibleEpsilon(bdd from);
bdd AccessibleEpsilon2(bdd from);
bdd AccessibleEpsilon(const bdd& from_s) const;
bdd AccessibleEpsilon2(const bdd& from_s) const;
// SOG generation
std::stack<std::pair<ClassOfState*, bdd>> RecherchePointsEntree(chem path,
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment