From 614529170217278a45102cd7b73cac3902839fa7 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Wed, 21 Oct 2020 11:19:41 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20CMakeLists.txt=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/ModelCheckerCPPThread.cpp=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/ModelCheckerTh.cpp=20=09supprim?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20src/ModelCheckerThV2.cpp?=
=?UTF-8?q?=20=09supprim=C3=A9=C2=A0:=20=20=20=20=20=20=20=20src/ModelChec?=
=?UTF-8?q?kerThV2.h?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
CMakeLists.txt | 6 +-
src/ModelCheckerCPPThread.cpp | 7 +-
src/ModelCheckerTh.cpp | 2 +-
src/ModelCheckerThV2.cpp | 215 ----------------------------------
src/ModelCheckerThV2.h | 34 ------
5 files changed, 6 insertions(+), 258 deletions(-)
delete mode 100644 src/ModelCheckerThV2.cpp
delete mode 100644 src/ModelCheckerThV2.h
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 494378e..3ef9451 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -12,7 +12,7 @@ set(CMAKE_CXX_EXTENSIONS OFF)
# Add compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g0 -falign-functions -falign-jumps -falign-loops -falign-labels -freorder-blocks -freorder-blocks-algorithm=stc -freorder-blocks-and-partition -fprefetch-loop-arrays -foptimize-strlen -fcaller-saves -finline-functions -funswitch-loops -fpermissive -std=c++17 -pthread")
endif()
@@ -26,7 +26,7 @@ add_subdirectory(${PARSER_DIR})
# build spot if it is not installed on the system
find_library(SPOT_LIBRARY "spot")
-find_library(BDDX_LIBRARY "bddx")
+
if(NOT SPOT_LIBRARY)
include(ExternalProject)
@@ -46,7 +46,7 @@ if(NOT SPOT_LIBRARY)
include_directories("${SPOT_DIR}/include")
else ()
message(STATUS "Found spot: ${SPOT_LIBRARY}")
- message(STATUS "Found bddx: ${BDDX_LIBRARY}")
+
find_path(SPOT_INCLUDE_PATH "spot")
include_directories("${SPOT_INCLUDE_PATH}")
diff --git a/src/ModelCheckerCPPThread.cpp b/src/ModelCheckerCPPThread.cpp
index d49fb19..6ad7a5a 100644
--- a/src/ModelCheckerCPPThread.cpp
+++ b/src/ModelCheckerCPPThread.cpp
@@ -30,7 +30,7 @@ void ModelCheckerCPPThread::preConfigure()
if ( max > getMaxMemoryV3() ) {
max = getMaxMemoryV3() /10*9;
}*/
- SylvanWrapper::sylvan_set_limits ( 16LL<<30, 8, 0 );
+ SylvanWrapper::sylvan_set_limits ( 16LL<<30, 10, 0 );
//sylvan_init_package();
SylvanWrapper::sylvan_init_package();
@@ -59,8 +59,8 @@ void ModelCheckerCPPThread::preConfigure()
}
m_initialMarking = SylvanWrapper::lddmc_cube ( liste_marques, m_net->places.size() );
-
SylvanWrapper::lddmc_refs_push ( m_initialMarking );
+
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc = new uint32_t[m_nbPlaces];
// Transition relation
@@ -117,9 +117,6 @@ void ModelCheckerCPPThread::Compute_successors()
if ( id_thread == 0 ) {
LDDState *c = new LDDState;
MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
- /*SylvanWrapper::getMarksCount(Complete_meta_state);
- exit(0);*/
-
SylvanWrapper::lddmc_refs_push ( Complete_meta_state );
fire = firable_obs ( Complete_meta_state );
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 3972099..a5aecf1 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -14,7 +14,7 @@ getMaxMemory()
}
void ModelCheckerTh::preConfigure() {
- SylvanWrapper::sylvan_set_limits ( 16LL<<29, 8, 0 );
+ SylvanWrapper::sylvan_set_limits ( 16LL<<30, 10, 0 );
SylvanWrapper::sylvan_init_package();
SylvanWrapper::sylvan_init_ldd();
SylvanWrapper::init_gc_seq();
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
deleted file mode 100644
index 8898951..0000000
--- a/src/ModelCheckerThV2.cpp
+++ /dev/null
@@ -1,215 +0,0 @@
-#include "ModelCheckerThV2.h"
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
-#include <functional>
-#include <iostream>
-#include <fstream>
-#include "SylvanWrapper.h"
-#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
-using namespace sylvan;
-using namespace std;
-
-ModelCheckerThV2::ModelCheckerThV2 ( const NewNet &R, int nbThread ) :
- ModelCheckBaseMT ( R, nbThread )
-{
-}
-size_t
-getMaxMemoryV3()
-{
- long pages = sysconf ( _SC_PHYS_PAGES );
- long page_size = sysconf ( _SC_PAGE_SIZE );
- return pages * page_size;
-}
-void ModelCheckerThV2::preConfigure()
-{
-
- lace_init ( m_nb_thread, 0 );
- lace_startup ( 0, NULL, NULL );
- size_t max = 16LL<<34;
- if ( max > getMaxMemoryV3() ) {
- max = getMaxMemoryV3() /10*9;
- }
- sylvan_set_limits ( 16LL<<29, 8, 0 );
-
- sylvan_init_package();
- sylvan_init_ldd();
- init_gc_seq();
- displayMDDTableInfo();
- vector<Place>::const_iterator it_places;
- m_transitions = m_net->transitions;
- m_observable = m_net->Observable;
- m_place_proposition = m_net->m_formula_place;
- m_nonObservable = m_net->NonObservable;
-
- m_transitionName = m_net->transitionName;
- m_placeName = m_net->m_placePosName;
-
- InterfaceTrans = m_net->InterfaceTrans;
-
- cout << "Nombre de places : " << m_nbPlaces << endl;
- cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
-
- uint32_t *liste_marques = new uint32_t[m_net->places.size()];
- uint32_t i;
- for ( i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++ ) {
- liste_marques[i] = it_places->marking;
- }
-
- m_initialMarking = lddmc_cube ( liste_marques, m_net->places.size() );
- ldd_refs_push ( m_initialMarking );
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc = new uint32_t[m_nbPlaces];
- // Transition relation
- for ( vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++ ) {
- // Initialisation
- for ( i = 0; i < m_nbPlaces; i++ ) {
- prec[i] = 0;
- postc[i] = 0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for ( vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++ ) {
- adjacentPlace.insert ( it->first );
- prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
- }
- // arcs post
- for ( vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++ ) {
- adjacentPlace.insert ( it->first );
- postc[it->first] = postc[it->first] + it->second;
-
- }
- for ( set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++ ) {
- MDD Precond = lddmc_true;
- Precond = Precond & ( ( *it ) >= prec[*it] );
- }
-
- MDD _minus = lddmc_cube ( prec, m_nbPlaces );
- ldd_refs_push ( _minus );
- MDD _plus = lddmc_cube ( postc, m_nbPlaces );
- ldd_refs_push ( _plus );
- m_tb_relation.push_back ( TransSylvan ( _minus, _plus ) );
- }
- delete[] prec;
- delete[] postc;
- ComputeTh_Succ();
-
-}
-
-
-
-
-void ModelCheckerThV2::Compute_successors()
-{
- int id_thread;
-
- id_thread = m_id_thread++;
-
- //cout<<" I'm here thread id " <<m_id_thread<<endl;
- Set fire;
-
- if ( id_thread == 0 ) {
- LDDState *c = new LDDState;
- MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
- /*SylvanWrapper::getMarksCount(Complete_meta_state);
- exit(0);*/
- ldd_refs_push ( Complete_meta_state );
- fire = firable_obs ( Complete_meta_state );
- c->m_lddstate = Complete_meta_state;
- c->setDeadLock ( Set_Bloc ( Complete_meta_state ) );
- c->setDiv ( Set_Div ( Complete_meta_state ) );
- m_graph->setInitialState ( c );
- m_graph->insert ( c );
- m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
- m_condStack.notify_one();
- m_finish_initial = true;
- }
- LDDState *reached_class;
- //pthread_barrier_wait ( &m_barrier_builder );
- Pair e;
- do {
- std::unique_lock<std::mutex> lk ( m_mutexStack );
- m_condStack.wait(lk,std::bind(&ModelCheckerThV2::hasToProcess,this));
- lk.unlock();
-
- if ( m_common_stack.try_pop ( e ) && !m_finish ) {
- while ( !e.second.empty() && !m_finish ) {
- int t = *e.second.begin();
- e.second.erase ( t );
- MDD reduced_meta = Accessible_epsilon ( get_successor ( e.first.second, t ) );
- ldd_refs_push ( reduced_meta );
- reached_class = new LDDState();
- reached_class->m_lddstate = reduced_meta;
- LDDState *pos = m_graph->find ( reached_class );
- if ( !pos ) {
- m_graph->addArc();
- m_graph->insert ( reached_class );
- fire = firable_obs ( reduced_meta );
- reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
- reached_class->setDiv ( Set_Div ( reduced_meta ) );
- m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
- m_condStack.notify_one();
- m_graph_mutex.lock();
- e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( reached_class, t ) );
- reached_class->Predecessors.insert ( reached_class->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
- m_graph_mutex.unlock();
- } else {
- delete reached_class;
- m_graph->addArc();
- m_graph_mutex.lock();
- e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( pos, t ) );
- pos->Predecessors.insert ( pos->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
- m_graph_mutex.unlock();
- }
-
- }
- e.first.first->setCompletedSucc();m_condBuild.notify_one();
- } //end advance
-
- } while ( !m_finish );
-
-
-}
-
-void ModelCheckerThV2::threadHandler ( void *context )
-{
- ( ( ModelCheckerThV2* ) context )->Compute_successors();
-}
-
-void ModelCheckerThV2::ComputeTh_Succ()
-{
-
- m_id_thread = 0;
-
-
-
- /* pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);*/
- pthread_barrier_init ( &m_barrier_builder, NULL, m_nb_thread + 1 );
-
- m_finish=false;
- for ( int i = 0; i < m_nb_thread; i++ ) {
- int rc;
- m_list_thread[i]= new thread ( threadHandler,this );
- if ( m_list_thread==nullptr ) {
- cout << "error: pthread_create, rc: " << rc << endl;
- }
- }
-}
-
-ModelCheckerThV2::~ModelCheckerThV2()
-{
- m_finish = true;
- m_condStack.notify_all();
- //pthread_barrier_wait ( &m_barrier_builder );
- for ( int i = 0; i < m_nb_thread; i++ ) {
- m_list_thread[i]->join();
- delete m_list_thread[i];
- }
-
-}
-bool ModelCheckerThV2::hasToProcess() const {
- return m_finish || !m_common_stack.empty();
-}
diff --git a/src/ModelCheckerThV2.h b/src/ModelCheckerThV2.h
deleted file mode 100644
index 610c13e..0000000
--- a/src/ModelCheckerThV2.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#ifndef MODELCHECKERTHV2_H
-#define MODELCHECKERTHV2_H
-#include "ModelCheckBaseMT.h"
-#include "stacksafe.h"
-#include "SafeDequeue.h"
-#include <atomic>
-#include <thread>
-#include <mutex>
-#include <condition_variable>
-typedef pair<LDDState *, int> couple_th;
-typedef stack<pair<LDDState *,int>> pile_t;
-
-class ModelCheckerThV2 : public ModelCheckBaseMT
-{
-public:
- ModelCheckerThV2(const NewNet &R,int nbThread);
- ~ModelCheckerThV2();
- static void threadHandler(void *context);
- void Compute_successors();
- void ComputeTh_Succ();
-private:
- void preConfigure();
- bool hasToProcess() const;
-
- SafeDequeue<Pair> m_common_stack;
- atomic<uint8_t> m_id_thread;
- std::mutex m_mutex;
- pthread_barrier_t m_barrier_builder;
- volatile bool m_finish=false;
- std::condition_variable m_condStack;
- std::mutex m_mutexStack;
- thread* m_list_thread[128];
-};
-#endif
--
GitLab