Skip to content
Snippets Groups Projects
Commit 4a86e618 authored by Kais Klai's avatar Kais Klai
Browse files

calcul poids chemins observés

parent 426b75cf
No related branches found
No related tags found
No related merge requests found
Pipeline #9549 failed with stage
......@@ -37,6 +37,16 @@ int Aggregate::WeightInOut(const int in, const int out) const {
return weight[PosTransInWeight(in)][PosTransOutWeight(out)];
}
Aggregate* Aggregate::GetsuccessorsOfTrans(int t) const
{
for (const Edge p : successors) {
if (p.transition == t) {
//std::cout<<"successor by "<<t<<" found"<<std::endl;
return p.state;
}
}
return nullptr;
}
Aggregate* Aggregate::GetPredecessorsOfTrans(const int t) const {
for (const Edge p : predecessors) {
if (p.transition == t) {
......
......@@ -89,6 +89,13 @@ class Aggregate {
*/
Aggregate* GetPredecessorsOfTrans(int t) const;
/**
* Return the successor of the aggregate by a given transition
* @param t transition identifier
* @return the predecessor of the aggregate
*/
Aggregate* GetsuccessorsOfTrans(int t) const;
/**
* Flag to indicate if the state was visited
*/
......
......@@ -261,7 +261,28 @@ void ComputeAbstractPaths(const string& net_file, int bound, bool only_sog,
// save generate SOG
SaveSOG(sog, output_file_prefix + "_sog.dot");
return;
//check weight obs paths
std::vector<std::string> obspath1;
obspath1.push_back(("t8"));
obspath1.push_back(("t11"));
obspath1.push_back(("t7"));
obspath1.push_back(("t10"));
std::vector<std::string> obspath2;
obspath2.push_back(("t7"));
obspath2.push_back(("t10"));
obspath2.push_back(("t8"));
obspath2.push_back(("t11"));
std::vector<std::vector<std::string>> listeObsPaths;
listeObsPaths.push_back(obspath1);
listeObsPaths.push_back(obspath2);
std::vector<int> res=pn_sog.ComputeWeightObsPaths(listeObsPaths,sog);
for(int w:res)
{
std::cout<<w<<std::endl;
}
return;
}
// compute the observable paths
......
......@@ -257,6 +257,7 @@ bdd PetriNetSOG::AccessibleEpsilon(const bdd &from) const {
return m2;
}
<<<<<<< HEAD
bdd PetriNetSOG::OneStepBackUnobs(const bdd &from,
const Aggregate *aggr) const {
bdd res = bdd_false();
......@@ -269,6 +270,9 @@ bdd PetriNetSOG::OneStepBackUnobs(const bdd &from,
return res;
}
=======
>>>>>>> 5cde081 (calcul poids chemins observés)
pair<int, bdd> PetriNetSOG::StepBackward(const bdd &from,
const Aggregate *aggr) const {
......@@ -303,7 +307,68 @@ Set PetriNetSOG::FirableObservableTrans(const bdd &from) const {
return res;
}
std::pair<bdd,set<int>> PetriNetSOG::OneStepBackUnobs(const bdd &from,
const Aggregate *aggr) const {
bdd res = bdd_false();
std::pair<bdd,set<int>> C;
//std::cout<<"One Step Back"<<std::endl;
set<int> fireBack;
for (const auto t : non_observables) {
bdd pred = relation[t][from]-from;
if((pred & aggr->bdd_state) != bdd_false()){
res = res | pred;
fireBack.insert(t);
//std::cout<<transitions[t].name<<std::endl;
}
}
C.first=res;
C.second=fireBack;
return C;
}
std::vector<int> PetriNetSOG::ComputeWeightObsPaths(std::vector<std::vector<string>> obsPaths, const SOG &g)
{
//std::cout<<"ICI compute weight obs paths"<<endl;
//std::cout<<obsPaths.size()<<" paths received"<<std::endl;
std::vector<int> w;
for(int i=0;i<obsPaths.size();i++)
w.push_back(0);
int cur=0;
//std::cout<<"ICI compute weight obs paths"<<endl;
for(std::vector<std::string> op: obsPaths)
{
//std::cout<<"Obs Ath"<<std::endl;
Aggregate *a=g.initial_state;
Aggregate *sa;
w[cur]+=ComputeSingleInitAggregate(g.initial_state, transitions_names[op[0]]);
for(int i=0;i<op.size()-1;i++)
{
//std::cout<<op[i]<<" ---> "<<op[i+1]<<std::endl;
sa=a->GetsuccessorsOfTrans(transitions_names[op[i]]);
w[cur]+=ComputeSingleWeight(sa,transitions_names[op[i]],transitions_names[op[i+1]]);
a=sa;
}
w[cur]+=op.size();
cur++;
}
return w;
}
int PetriNetSOG::ComputeSingleInitAggregate(const Aggregate *aggr, const int out)
{
bdd source = SearchExitPoints(aggr->bdd_state, out);
const bdd dest =m0;
int counter = 0;
while ((source & dest) == bdd_false()) {
std::pair<bdd,std::set<int>> step=OneStepBackUnobs(source, aggr);
source = step.first;
counter++;
}
return counter;
}
int PetriNetSOG::ComputeSingleWeight(const Aggregate *aggr, const int in,
const int out) const {
bdd source = SearchExitPoints(aggr->bdd_state, out);
......@@ -312,7 +377,8 @@ int PetriNetSOG::ComputeSingleWeight(const Aggregate *aggr, const int in,
// backtracking from t_target until t_source
int counter = 0;
while ((source & dest) == bdd_false()) {
source = OneStepBackUnobs(source, aggr);
std::pair<bdd,std::set<int>> step=OneStepBackUnobs(source, aggr);
source = step.first;
counter++;
}
......@@ -361,7 +427,7 @@ void PetriNetSOG::GenerateSOG(SOG &sog) const {
auto *succ_aggr = new Aggregate;
const bdd complete_succ_aggr =
AccessibleEpsilon(GetSuccessor(curr_aggr.aggregate->bdd_state, t));
AccessibleEpsilon(GetSuccessor(curr_aggr.aggregate->bdd_state, t));
succ_aggr->bdd_state = complete_succ_aggr;
Aggregate *pos = sog.FindState(succ_aggr);
......
......@@ -94,7 +94,15 @@ class PetriNetSOG {
* @param aggr transition identifier
* @return the set of reached states by a step backward
*/
bdd OneStepBackUnobs(const bdd& from, const Aggregate* aggr) const;
std::pair<bdd,set<int>> OneStepBackUnobs(const bdd& from, const Aggregate* aggr) const;
/**
* Computes the weight of each observable path
* @param obsPaths : a list of paths each represented by a vector of string (transitions composing the path)
* @return a vector containing the corresponding weights
*/
std::vector<int> ComputeWeightObsPaths(std::vector<std::vector<string>> obsPaths, const SOG& g);
/**
* Compute one row of the weight matrix corresponding to the input transition
......@@ -113,11 +121,22 @@ class PetriNetSOG {
*/
int ComputeSingleWeight(const Aggregate* aggr, int in, int out) const;
/**
* Transitive closure on unobserved transitions
* @param from marking from which the closure is computed
* @return the set of reached states
*/
/**
* Computes the weight (length of the shortest path) from the initial marking
* of the initial aggregate to leave it by output transition out
* @param aggr supposed to be the initial aggregate of the SOG
* @param out output transition
* @return the weight
* */
int ComputeSingleInitAggregate(const Aggregate *aggr, const int out);
/**
* Transitive closure on unobserved transitions
* @param from marking from which the closure is computed
* @return the set of reached states
*/
bdd AccessibleEpsilon(const bdd& from) const;
/**
......
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