DiaDes
0.1
DIAgnosis of Discrete-Event System
|
#include <iostream>
#include <vector>
#include <string>
#include <set>
#include <list>
#include <fstream>
#include "boost/date_time/posix_time/posix_time.hpp"
#include <utils/Random.hh>
#include <utils/Verbose.hh>
#include <utils/CmdInterface.hh>
#include <automata/ComposableModel.hh>
#include <automata/ObservableComponent.hh>
Go to the source code of this file.
Functions | |
vector< string > | fileExtensions (numberOfFileExtensions) |
vector< string > | options (numberOfOptions) |
vector< bool > | isSet (numberOfOptions, false) |
void | initialiseOptions () |
void | clean (vector< Diades::Automata::ObservableComponent *> &components, Diades::Automata::ComposableModel *model, vector< Diades::Automata::ComposableModel::ConstPointer > &comps) |
int | main (int argc, char **argv) |
Variables | |
unsigned | numberOfOptions = 2 |
unsigned | numberOfFileExtensions = 2 |
string | description ="Usage: dd-check-reachability --help | model1.des_comp [model2.des_comp ... sync.rules] [--event e1 e2 ]" |
enum FileExtension |
Enumerator | |
---|---|
DESCOMP | |
DESCOMP | |
RULES | |
DESCOMP | |
DESCOMP | |
RULES | |
XML | |
ABSTRACTION | |
DIAGNOSER | |
DESCOMP | |
ARCHV | |
DESCOMP | |
RULES | |
XML | |
DESCOMP | |
RULES | |
XML | |
RULES |
Definition at line 38 of file CheckReachability.cc.
enum Option |
Definition at line 37 of file CheckReachability.cc.
void clean | ( | vector< Diades::Automata::ObservableComponent *> & | components, |
Diades::Automata::ComposableModel * | model, | ||
vector< Diades::Automata::ComposableModel::ConstPointer > & | comps | ||
) |
Clean the allocated structure
components | the set of loaded components |
model | the composable model (if any) |
comps | the elementary composable models (if any) |
Definition at line 69 of file CheckReachability.cc.
References Diades::Utils::LoggerFactory::destroy(), and Diades::Automata::EventFactory::destroy().
Referenced by main().
vector<string> fileExtensions | ( | numberOfFileExtensions | ) |
Referenced by initialiseOptions(), and main().
void initialiseOptions | ( | ) |
Definition at line 48 of file CheckReachability.cc.
References DESCOMP, EVENT, fileExtensions(), HELP, options(), and RULES.
Referenced by main().
vector<bool> isSet | ( | numberOfOptions | , |
false | |||
) |
Referenced by main().
int main | ( | int | argc, |
char ** | argv | ||
) |
Main function of the program check-reachability
Basically, this function analyses the parameters to initiate the analysis
argc | the number of parameters |
argv | the list of parameters |
Definition at line 112 of file CheckReachability.cc.
References Diades::Automata::ObservableMask::addMask(), clean(), DESCOMP, description, EVENT, Diades::Automata::ObservableMask::eventEnd(), fileExtensions(), Diades::Utils::getFileExtension(), HELP, Diades::Graph::NodeMap< T >::init(), initialiseOptions(), isSet(), numberOfOptions, Diades::Automata::ObservableMask::observableBegin(), options(), printError(), printUsage(), RULES, Diades::Utils::saveLog(), and Diades::Automata::Experimental::toDot().
vector<string> options | ( | numberOfOptions | ) |
Referenced by initialiseOptions(), and main().
string description ="Usage: dd-check-reachability --help | model1.des_comp [model2.des_comp ... sync.rules] [--event e1 e2 ]" |
Definition at line 46 of file CheckReachability.cc.
Referenced by main().
unsigned numberOfFileExtensions = 2 |
Definition at line 40 of file CheckReachability.cc.
unsigned numberOfOptions = 2 |
Definition at line 39 of file CheckReachability.cc.
Referenced by main().