diff --git a/README.md b/README.md
index 184ba651ac78d98e28adc15caab2d81c6016a79e..a721e0e292b7521d502d7110552624c68d8a0177 100644
--- a/README.md
+++ b/README.md
@@ -50,7 +50,7 @@ arg1: specifies method of creating threads. It can be set with one of the follow
* lc : using lace framework and applying canonization on nodes
arg2: specifies the number of threads/workers to be created
arg3: specifies the net to build its SOG
-arg4: specifies the LTL formula
+arg4: specifies the LTL formula file
```
diff --git a/src/LDDStateExtend.cpp b/src/LDDStateExtend.cpp
deleted file mode 100644
index 1bf6d3652c879e1be30db29bd7a0fe69bfdb5a2b..0000000000000000000000000000000000000000
--- a/src/LDDStateExtend.cpp
+++ /dev/null
@@ -1,13 +0,0 @@
-#include "LDDStateExtend.h"
-
-
-LDDStateExtend::~LDDStateExtend()
-{
- //dtor
-}
-void LDDStateExtend::setLDDExValue(MDD m) {
- m_lddstate=m;
-}
-MDD LDDStateExtend::getLDDExValue() {
- return m_lddstate;
-}
diff --git a/src/LDDStateExtend.h b/src/LDDStateExtend.h
deleted file mode 100644
index a2a98706ba1e2446c5ec5ca262a11df5b87ac6d4..0000000000000000000000000000000000000000
--- a/src/LDDStateExtend.h
+++ /dev/null
@@ -1,30 +0,0 @@
-#ifndef LDDSTATEEXTEND_H_INCLUDED
-#define LDDSTATEEXTEND_H_INCLUDED
-
-#include <set>
-#include <vector>
-#include <sylvan.h>
-#include "LDDState.h"
-using namespace std;
-
-typedef set<int> Set;
-
-class LDDStateExtend: public LDDState
-{
- public:
- LDDStateExtend(){m_boucle=m_blocage=m_visited=false;}
- virtual ~LDDStateExtend();
- bool m_exist;
-
- void setLDDExValue(MDD m);
- MDD getLDDExValue();
-
- protected:
-
- private:
-
-};
-typedef pair<LDDStateExtend*, int> LDDExEdge;
-typedef vector<LDDEdge> LDDExEdgedges;
-
-#endif // LDDSTATEEXTEND_H_INCLUDED
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..b1fa51415c0ba28d95b4dcda4266a31928df043a
--- /dev/null
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -0,0 +1,67 @@
+#include <spot/kripke/kripke.hh>
+#include "LDDGraph.h"
+#include "SogKripkeStateOTF.h"
+#include "SogKripkeIteratorOTF.h"
+
+
+SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDGraph& m_gr, const SogKripkeStateOTF& lddstate, bdd cnd):m_sog(m_gr),m_lddstate(lddstate), kripke_succ_iterator(cnd)
+{
+ //vector<pair<LDDState*, int>>
+ m_lddstate->setDiv(true);
+ for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
+ m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
+ }
+ /* if (lddstate->isDeadLock()) {
+ m_lsucc.push_back(pair(,-1));
+ }*/
+ if (lddstate->isDiv()) {
+ m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+ }
+}
+bool SogKripkeIteratorOTF::first() {
+ // m_sog->getLDDStateById(m_id)->Successors().
+ //return m_sog->get_successor()
+
+ m_current_edge=0;
+ return m_lsucc.size()!=0;
+}
+
+bool SogKripkeIteratorOTF::next() {
+
+ m_current_edge++;
+ return m_current_edge<m_lsucc.size();
+}
+
+bool SogKripkeIteratorOTF::done() const {
+
+ return m_current_edge==m_lsucc.size();
+}
+
+SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
+ {
+ return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
+ }
+
+bdd SogKripkeIteratorOTF::cond() const {
+ if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+ string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
+ //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
+
+ spot::bdd_dict *p=m_dict_ptr->get();
+ spot::formula f=spot::formula::ap(name);
+ bdd result=bdd_ithvar((p->var_map.find(f))->second);
+
+ //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";*/
+ //return result;
+ return result;
+}
+
+/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+ //cout<<"Iterator acc()\n";
+ return 0U;
+}*/
+SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
+{
+ //dtor
+}
+
diff --git a/src/SogKripkeIteratorOTF.h b/src/SogKripkeIteratorOTF.h
new file mode 100644
index 0000000000000000000000000000000000000000..d1f191a97fed2fec0df57565c055e0b2edcd94cc
--- /dev/null
+++ b/src/SogKripkeIteratorOTF.h
@@ -0,0 +1,56 @@
+#ifndef SOGKRIPKEITERATOROTF_H_INCLUDED
+#define SOGKRIPKEITERATOROTF_H_INCLUDED
+#include "SogKripkeStateOTF.h"
+#include "LDDGraph.h"
+#include <spot/kripke/kripke.hh>
+// Iterator for a SOG graph
+class SogKripkeIteratorOTF : public spot::kripke_succ_iterator
+{
+public:
+
+ // static LDDGraph * m_graph;
+ static spot::bdd_dict_ptr* m_dict_ptr;
+ // sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
+ SogKripkeIteratorOTF(const LDDGraph& m_gr, const SogKripkeStateOTF& lddstate, bdd cnd);
+ virtual ~SogKripkeIteratorOTF();
+ bool first() override;
+ bool next() override;
+ bool done() const override;
+ SogKripkeStateOTF* dst() const override;
+ bdd cond() const override final;
+
+ SogKripkeStateOTF* current_state() const;
+
+ bdd current_condition() const;
+
+ int current_transition() const;
+
+ bdd current_acceptance_conditions() const;
+
+ std::string format_transition() const;
+
+private:
+ //const threadSOG& pn_sog; ///< The petri net.
+ MDD from; ///< The source state.
+ bool dead; ///< The source div attribut.
+ bool div; ///< The source div attribut.
+ // bdd cond; ///< The condition which must label all successors.
+
+ std::set<int>::const_iterator it;
+ /// \brief Designate the associated Petri net.
+ // const SogKripkeOTF& pn_sog;
+
+ /// \brief Point to the marking for which we iterate.
+ //MDD mark;
+ // Associated SOG graph
+
+ LDDState * m_lddstate;
+ LDDGraph *m_sog;
+ vector<pair<SogKripkeStateOTF, int>> m_lsucc;
+ unsigned int m_current_edge=0;
+ LDDGraph * SogKripkeIteratorOTF::m_graph;
+ // spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
+};
+
+
+#endif // SOGKRIPKEITERATOR_H_INCLUDED
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..dafb02769abdcbfcb1319dc365003efdf7fc92e4
--- /dev/null
+++ b/src/SogKripkeOTF.cpp
@@ -0,0 +1,79 @@
+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/kripke/kripke.hh>
+#include <spot/twa/bdddict.hh>
+
+
+#include "SogKripkeIteratorOTF.h"
+#include "SogKripkeStateOTF.h"
+
+#include "SogKripkeOTF.h"
+#include <map>
+using namespace spot;
+SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(dict_ptr),m_sog(sog)
+{
+ SogKripkeIteratorOTF::m_graph=sog;
+ SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
+}
+
+SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(dict_ptr,sog) {
+ for (auto it=l_transap.begin();it!=l_transap.end();it++) {
+ register_ap(*it);
+ }
+ for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
+ register_ap(*it);
+}
+
+
+state* SogKripkeOTF::get_init_state() const {
+ //cout<<"Initial state given...\n";
+ return new SogKripkeStateOTF(m_sog->getInitialState());//new SpotSogState();
+
+}
+// Allows to print state label representing its id
+std::string SogKripkeOTF::format_state(const spot::state* s) const
+ {
+ auto ss = static_cast<const SogKripkeStateOTF*>(s);
+ std::ostringstream out;
+ out << "( " << ss->getLDDState()->getLDDValue() << ")";
+ cout << "( " << ss->getLDDState()->getLDDValue() << ")";
+ return out.str();
+ }
+
+SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const {
+
+ auto ss = static_cast<const SogKripkeStateOTF*>(s);
+ //////////////////////////////////////////////
+
+ return new SogKripkeIteratorOTF(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
+}
+
+bdd SogKripkeOTF::state_condition(const spot::state* s) const
+ {
+
+ auto ss = static_cast<const SogKripkeStateOTF*>(s);
+ vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+
+
+ bdd result=bddtrue;
+ // Marked places
+ for (auto it=marked_place.begin();it!=marked_place.end();it++) {
+ string name=m_sog->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+ vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+ for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
+ string name=m_sog->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+ return result;
+ }
+
+
+SogKripkeOTF::~SogKripkeOTF()
+{
+ //dtor
+}
+
diff --git a/src/SogKripkeOTF.h b/src/SogKripkeOTF.h
new file mode 100644
index 0000000000000000000000000000000000000000..300e783f5fd888940c1dcab08c787c601574f36b
--- /dev/null
+++ b/src/SogKripkeOTF.h
@@ -0,0 +1,34 @@
+#ifndef SOGKRIPKEOTF_H_INCLUDED
+#define SOGKRIPKEOTF_H_INCLUDED
+#include "LDDGraph.h"
+#include "SogKripkeIteratorOTF.h"
+#include <spot/kripke/kripke.hh>
+#include <LDDGraph.h>
+#include <NewNet.h>
+
+
+class SogKripkeOTF: public spot::kripke {
+ public:
+
+ //SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
+ SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,const NewNet *n,set<string> &l_transap,set<string> &l_placeap);
+ virtual ~SogKripkeOTF();
+ spot::state* get_init_state() const;
+ SogKripkeIteratorOTF* succ_iter(const spot::state* s) const override;
+ std::string format_state(const spot::state* s) const override;
+ bdd state_condition(const spot::state* s) const override;
+
+ /// \brief Get the graph associated to the automaton.
+ const LDDGraph& get_graph() const {
+ return *m_sog;
+ }
+ LDDGraph *m_sog;
+
+ protected:
+
+ private:
+ std::map<int, int> place_prop;
+ //LDDGraph* m_sog;
+};
+
+#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/SogKripkeStateOTF.cpp b/src/SogKripkeStateOTF.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..c86bc26d9ebfbe2c49862804812a18e7e3356f7c
--- /dev/null
+++ b/src/SogKripkeStateOTF.cpp
@@ -0,0 +1,40 @@
+#include <spot/kripke/kripke.hh>
+#include "LDDState.h"
+#include "SogKripkeStateOTF.h"
+
+
+SogKripkeStateOTF::~SogKripkeStateOTF()
+{
+ //dtor
+}
+SogKripkeStateOTF::SogKripkeStateOTF(const MDD& m)
+ : spot::state(), ma(m)
+{
+} //
+
+
+SogKripkeStateOTF* SogKripkeStateOTF::clone() const
+{
+ return new SogKripkeStateOTF(*this);
+}
+
+size_t SogKripkeStateOTF::hash() const
+{
+ return m_state->getLDDValue();
+}
+
+int SogKripkeStateOTF::compare(const spot::state* other) const
+{
+ auto o = static_cast<const SogKripkeStateOTF*>(other);
+ size_t oh = o->hash();
+ size_t h = hash();
+ if (h < oh)
+ return -1;
+ else
+ return h > oh;
+}
+
+const MDD& SogKripkeStateOTF::get_marking() const
+{
+ return ma;
+} //
diff --git a/src/SogKripkeStateOTF.h b/src/SogKripkeStateOTF.h
new file mode 100644
index 0000000000000000000000000000000000000000..674ce257d298dd22bf99c0a4d6fa1c75d01865b0
--- /dev/null
+++ b/src/SogKripkeStateOTF.h
@@ -0,0 +1,32 @@
+#ifndef SOGKRIPKESTATEOTF_H_INCLUDED
+#define SOGKRIPKESTATEOTF_H_INCLUDED
+
+
+#include "LDDState.h"
+
+class SogKripkeStateOTF : public spot::state
+{
+public:
+ SogKripkeStateOTF(const MDD &m);
+ virtual ~SogKripkeStateOTF();
+
+ SogKripkeStateOTF* clone() const override;
+ size_t hash() const override;
+
+ int compare(const spot::state* other) const override;
+
+ LDDState* getLDDState()
+ {
+ return m_state;
+ }
+ const MDD& get_marking() const;
+ double limit_marking(const bdd& m);
+
+
+private:
+ LDDState *m_state;
+ MDD ma;
+};
+
+
+#endif // SOGKRIPKESTATE_H_INCLUDED
diff --git a/src/main.cpp b/src/main.cpp
index 6b4c00478087e92225ae7e2f08b3a31d3711ff4b..5c4333cbca9a563ff79ef6e6e82519eec8ee5a8c 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -124,7 +124,28 @@ int main(int argc, char** argv)
MPI_Comm_rank(MPI_COMM_WORLD,&task_id);
//
- if (n_tasks==1)
+ if (n_tasks==1 && !strcmp(argv[1],"otf"))
+ {
+ cout<<"Multi-threaded on the fly Model checking..."<<endl;
+ cout<<"Building automata for not(formula)\n";
+ auto d = spot::make_bdd_dict();
+ // d->register_ap("jbhkj");
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ cout<<"Formula automata built.\n";
+ cout<<"Want to save the graph in a dot file ?";
+ char c;
+ cin>>c;
+ if (c=='y')
+ {
+ fstream file;
+ string st(formula);
+ st+=".dot";
+ file.open(st.c_str(),fstream::out);
+ spot::print_dot(file, af);
+ file.close();
+ }
+ }
+ else if (n_tasks==1)
{
cout<<"number of task = 1 \n " <<endl;
bool uselace=(!strcmp(argv[1],"lc")) || (!strcmp(argv[1],"l"));
@@ -176,12 +197,13 @@ int main(int argc, char** argv)
{
cout<<"Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
- // d->register_ap("jbhkj");
+ // d->register_ap("jbhkj");
spot::twa_graph_ptr af = spot::translator(d).run(not_f);
cout<<"Formula automata built.\n";
cout<<"Want to save the graph in a dot file ?";
cin>>c;
- if (c=='y') {
+ if (c=='y')
+ {
fstream file;
string st(formula);
st+=".dot";
@@ -192,14 +214,15 @@ int main(int argc, char** argv)
//auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
spot::twa_graph_ptr k =
- spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()),
- spot::twa::prop_set::all(), true);
+ spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()),
+ spot::twa::prop_set::all(), true);
cout<<"SOG translated to SPOT succeeded.."<<endl;
cout<<"Want to save the graph in a dot file ?";
cin>>c;
- if (c=='y') {
+ if (c=='y')
+ {
fstream file;
string st(argv[3]);
@@ -208,7 +231,8 @@ int main(int argc, char** argv)
spot::print_dot(file, k,"ka");
file.close();
}
- if (auto run = k->intersecting_run(af)) {
+ if (auto run = k->intersecting_run(af))
+ {
/*std::cout << "formula is violated by the following run:\n" << *run;*/
run->highlight(5); // 5 is a color number.
fstream file;
@@ -216,12 +240,12 @@ int main(int argc, char** argv)
cout<<"xxxxxxxxxxxxxxxxxx"<<endl;
spot::print_dot(file, k, ".kA");
file.close();
- }
+ }
else
std::cout << "formula is verified\n";
}
- }
+ }
}