diff --git a/src/.MCHybridSOG.h.kate-swp b/src/.MCHybridSOG.h.kate-swp
new file mode 100644
index 0000000000000000000000000000000000000000..a65057426854c2e2438dac15c8c74a0492744abb
Binary files /dev/null and b/src/.MCHybridSOG.h.kate-swp differ
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2f27223ccf21036a6f7ba53785b85bcf7d745468..4231a5f4049a99848bcad77aa9f95f6f12914afe 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -9,16 +9,27 @@ include_directories(${MPI_INCLUDE_PATH})
find_package(OpenSSL)
include_directories(${OPENSSL_INCLUDE_DIR})
-# include spot library
-add_library(spot STATIC IMPORTED)
-set_target_properties(spot PROPERTIES IMPORTED_LOCATION "${SPOT_DIR}/lib/libspot.a")
+include_directories("${CMAKE_SOURCE_DIR}/third-party/sylvan/src")
+
+
+add_library(spot SHARED IMPORTED) # or STATIC instead of SHARED
+set_target_properties(spot PROPERTIES
+ IMPORTED_LOCATION "/usr/lib/x86_64-linux-gnu/libspot.so"
+ INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
+)
+
+add_library(bddx SHARED IMPORTED) # or STATIC instead of SHARED
+set_target_properties(bddx PROPERTIES
+ IMPORTED_LOCATION "/usr/lib/x86_64-linux-gnu/libbddx.so"
+ INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
+)
+
+
+
-# include bddx library
-add_library(bddx STATIC IMPORTED)
-set_target_properties(bddx PROPERTIES IMPORTED_LOCATION "${SPOT_DIR}/lib/libbddx.a")
# Hybrid SOG executable
-add_executable(pmc-sog main.cpp
+add_executable(hybrid-sog main.cpp
NewNet.cpp
NewNet.h
CommonSOG.cpp
@@ -69,7 +80,7 @@ add_executable(pmc-sog main.cpp
HybridKripkeState.h
)
-target_link_libraries(pmc-sog
+target_link_libraries(hybrid-sog
bddx
spot
sylvan
@@ -77,5 +88,3 @@ target_link_libraries(pmc-sog
${MPI_LIBRARIES}
${OPENSSL_LIBRARIES}
)
-
-add_dependencies(pmc-sog SpotLibrary)
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 1ed2bc9514f27cedf05c27c498cfda25fb125db2..c0d31b827933bc243cb8b51b62685e4a1d8edd7a 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -567,13 +567,10 @@ void MCHybridSOG::read_message()
uint16_t id_p=i_agregate->getProcess();
memcpy(message+16,&id_p,2);
MPI_Send(message,22,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD);
- break;
-
-
-
- default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
+ break;
+ /*default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
//AbortTerm();
- break;
+ //break; */
}
MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status);
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 2db8f3ee6a2f30fa8a5402b0a47d7751fe35f6b5..740269a8874e69f96aaf8ace39cb722bdbb18e81 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -33,7 +33,7 @@ void ModelCheckLace::preConfigure() {
print_h(max);
printf(" max.\n");
LACE_ME;
- sylvan_set_limits(max, 16, 2);
+ sylvan_set_limits(max, 16, 1);
sylvan_init_package();
sylvan_init_ldd();
@@ -58,7 +58,7 @@ void ModelCheckLace::preConfigure() {
cout<<(*it2).first<<" : "<<(*it2).second<<endl;
}*/
//cout<<"Transitions observables :"<<endl;
- Set::iterator it=m_observable.begin();
+ //Set::iterator it=m_observable.begin();
/*for (; it!=m_observable.end(); it++)
{
cout<<*it<<" ";
@@ -133,20 +133,16 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
{
MDD M1;
MDD M2=From;
- int it=0;
- /*lddmc_refs_pushptr(&M1);
- lddmc_refs_pushptr(&M2);*/
- cout<<"worker "<<lace_get_worker()->worker<<endl;
-
+
do
{
M1=M2;
- for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
+ for(Set::iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
{
lddmc_refs_spawn(SPAWN(lddmc_firing_lace,M2,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus()));
}
- for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
+ for(Set::iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
{
lddmc_refs_push(M1);
lddmc_refs_push(M2);
@@ -155,6 +151,8 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
M2=lddmc_union(succ,M2);
lddmc_refs_pop(3);
}
+ cout<<"M1 :"<<M1<<endl;
+ cout<<"M2 :"<<M2<<endl;
}
while (M1!=M2);
@@ -237,7 +235,7 @@ LDDState * ModelCheckLace::getInitialMetaState()
// Compute successors
unsigned int onb_it=0;
Set::iterator iter=fire.begin();
- int j=0;
+
while(iter!=fire.end())
{
diff --git a/src/main.cpp b/src/main.cpp
index 0975099083c9bc96c38003e88f3441a4c01e095a..eca281346f06e7a281f69f555b46f53ee8660f65 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -349,19 +349,8 @@ int main(int argc, char** argv)
auto d = spot::make_bdd_dict();
spot::twa_graph_ptr af = spot::translator(d).run(not_f);
-
- /* spot::twa_graph_ptr k =spot::make_twa_graph(std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet),spot::twa::prop_set::all(), true);
- cout<<"finished...."<<endl;
-
-
- fstream file;
- string st(argv[3]);
- st+=".dot";
- file.open(st.c_str(),fstream::out);
- spot::print_dot(file, k,"ka");
- file.close(); */
+
double tps;
-
auto t1 = std::chrono::high_resolution_clock::now();
auto k =
std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet);
@@ -372,9 +361,7 @@ int main(int argc, char** argv)
std::cout << "temps de verification "
<< std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
<< " milliseconds\n";
-
cout<<"=================================="<<endl;
-
}
else
{
@@ -385,27 +372,19 @@ int main(int argc, char** argv)
<< " milliseconds\n";
}
-
}
-
}
-
-
}
else
- {
- //cout<<" sequential version using Sylvan : 1 with BuDDy : 2 \n" <<endl;
+ {
cout<<"*************Distibuted version******************* \n" <<endl;
{
DistributedSOG DR(Rnewnet, bound);
LDDGraph g(nullptr);
DR.computeDSOG(g);
}
-
-
}
}
-
MPI_Finalize();
return (EXIT_SUCCESS);
}
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
index 152af82e6f2189ba66ea1d811df06cb3a8b15e6e..80424bb29686816f757e0bb943266d1dc8e056f7 100644
--- a/src/sylvan_sog.c
+++ b/src/sylvan_sog.c
@@ -66,7 +66,8 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
MDD left=lddmc_refs_sync(SYNC(lddmc_firing_lace));
lddmc_refs_push(left);
MDD result2 =
- lddmc_makenode(l_values[count],left, lddmc_false);
+ lddmc_makenode(l_values[count],left, lddmc_false);
+ if (l_values[count]>5) printf("%d ",l_values[count]);
lddmc_refs_push(result2);
result = lddmc_union( result, result2);
lddmc_refs_pop(3);