DiaDes
0.1
DIAgnosis of Discrete-Event System
|
This file implements the dd-tagstates command that is used to tag a set of states (initial, final) from an automaton (ddaut format) based on regular expressions. More...
#include <cstdlib>
#include <iostream>
#include <fstream>
#include <regex>
#include <unordered_map>
#include <boost/program_options.hpp>
#include <diades/automata/experimental/AutFile.hh>
#include <diades/automata/experimental/DdAutFile.hh>
#include "../AutomataInterface.hh"
#include "diades/automata/experimental/DdAutFileDescriptor.hh"
#include <diades/automata/experimental/Io.hh>
Go to the source code of this file.
Enumerations | |
enum | Tag { final, nofinal, initial, noinitial, prefixclosedfinal, swapfinal, swapinitial } |
Functions | |
const string | program ("dd-tagstates") |
const string | briefcomment (": this program tags some states based on regular expressions (output file or standard output).") |
void | initialiseOptions (int argc, char *argv[], Poptions::options_description &desc, Poptions::variables_map &vm) |
void | applyTag (DdAutFA &fa, DdAutFA::State state, Tag tag) |
void | getReachable (DdAutFA &fa, CstStMap< char > &mapping, std::regex ®, DdAutStateManager &sManager, std::list< DdAutFA::State > &acceptors) |
void | tagPredecessors (DdAutFA &fa, std::list< DdAutFA::State > &acceptors, CstStMap< char > &mapping) |
void | setPrefixClosedAcceptorTag (DdAutFA &fa, DdAutStateManager &sManager, std::regex ®) |
void | tagStates (DdAutFA &fa, DdAutStateManager &sManager, const std::string &expr) |
size_t | tagDdAutStates2 (const string &fileName, const string &output, const std::vector< std::string > ®exp) |
size_t | tagDdAutStates (const string &fileName, const string &output, const std::vector< std::string > ®exp) |
int | main (int argc, char **argv) |
Variables | |
const string | detailedcomment |
FileSuffixes | suffixes ({"ddaut"}) |
const std::unordered_map< std::string, Tag > | tagOf |
This file implements the dd-tagstates command that is used to tag a set of states (initial, final) from an automaton (ddaut format) based on regular expressions.
dd-tagstates tags a set of states to be initial or final based on a regular expression. regular expression are defined as proposed in http://www.cplusplus.com/reference/regex/ECMAScript/
Example 1: set to be acceptor any states such that its label contains the substring 'o.p=ko'
dd-tagstates file.ddaut -r 'final:.*o\.p=ko.*'
Example 2: set to be non-acceptor any states such that its label contains the substring 'o.p=ok'
dd-tagstates file.ddaut -r 'nofinal:.*o\.p=ok.*'
Example 3: set to be initial any states such that its label contains the substring 'init'
dd-tagstates file.ddaut -r 'initial:.*init.*'
Example 4: set to be not initial any states such that its label is 's1' or 's2' or 's3'
dd-tagstates file.ddaut -r 'noinitial:s[1-3]'
Applying Example 5: applying Examples 1-4 in one go. Tagging works from left to right, we tag first 'final:.*o.p=ko.*' then -r 'nofinal:.*o.p=ok.*' so the order matters.
dd-tagstates file.ddaut -r 'final:.*o\.p=ko.*' -r 'nofinal:.*o\.p=ok.*' -r 'initial:.*init.*' -r 'noinitial:s[1-3]'
Example 6: tag a set of states S as acceptors and tag other states so that any prefix of a word accepted by a state of S is also an accepted word.
dd-tagstates file.ddaut -r 'prefix-closed-final:.*o\.p=ko.*'
Example 7: swap the tags of the set of states S: swap-final if the state is final swap to non-final, if the state is final then swap to final. swap-initial if the state is initial swap to non-initial, if the state is non-initial then swap to initial.
dd-tagstates file.ddaut -r 'swap-final:.*o\.p=ko.*' 'swap-initial:.*o\.p=ok.*'
Definition in file TagStates.cc.
enum Tag |
Enumerator | |
---|---|
final | |
nofinal | |
initial | |
noinitial | |
prefixclosedfinal | |
swapfinal | |
swapinitial |
Definition at line 160 of file TagStates.cc.
void applyTag | ( | DdAutFA & | fa, |
DdAutFA::State | state, | ||
Tag | tag | ||
) |
Definition at line 173 of file TagStates.cc.
References initial, nofinal, noinitial, prefixclosedfinal, Diades::Automata::Experimental::FiniteAutomaton< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::setAcceptingState(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::setInitial(), Diades::Automata::Experimental::FiniteAutomaton< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::swapAcceptingState(), swapfinal, swapinitial, Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::swapInitialState(), Diades::Automata::Experimental::FiniteAutomaton< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::unsetAcceptingState(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::unsetInitial().
Referenced by tagPredecessors(), and tagStates().
const string briefcomment | ( | ": this program tags some states based on regular expressions (output file or standard output)." | ) |
Referenced by main().
void getReachable | ( | DdAutFA & | fa, |
CstStMap< char > & | mapping, | ||
std::regex & | reg, | ||
DdAutStateManager & | sManager, | ||
std::list< DdAutFA::State > & | acceptors | ||
) |
Definition at line 188 of file TagStates.cc.
References current, Diades::Automata::Experimental::StatePropertyManager< _StateProperty, _StatePropertyId, NullStProperty, NullStPropertyId, Hash >::getStateProperty(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getStatePropertyId(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::initialStateEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::outputTransitionBegin(), and Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::outputTransitionEnd().
Referenced by setPrefixClosedAcceptorTag().
void initialiseOptions | ( | int | argc, |
char * | argv[], | ||
Poptions::options_description & | desc, | ||
Poptions::variables_map & | vm | ||
) |
Initialise the options of the command present in the command line
argc | |
argv | |
desc | |
vm |
Definition at line 129 of file TagStates.cc.
References options().
Referenced by main().
int main | ( | int | argc, |
char ** | argv | ||
) |
Main file of the dd-dot command
argc | |
argv |
Definition at line 381 of file TagStates.cc.
References briefcomment(), detailedcomment, initialiseOptions(), Diades::CmdInterface::printCommandLineError(), printUsage(), program(), and tagDdAutStates().
const string program | ( | "dd-tagstates" | ) |
Referenced by main().
void setPrefixClosedAcceptorTag | ( | DdAutFA & | fa, |
DdAutStateManager & | sManager, | ||
std::regex & | reg | ||
) |
Definition at line 262 of file TagStates.cc.
References Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::behaviour(), getReachable(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::numberOfStates(), and tagPredecessors().
Referenced by tagStates().
size_t tagDdAutStates | ( | const string & | fileName, |
const string & | output, | ||
const std::vector< std::string > & | regexp | ||
) |
Definition at line 352 of file TagStates.cc.
References ERROR_UNHANDLED_EXCEPTION, Diades::CmdInterface::FileSuffixes::match(), Diades::CmdInterface::printCommandLineError(), suffixes, and tagDdAutStates2().
Referenced by main().
size_t tagDdAutStates2 | ( | const string & | fileName, |
const string & | output, | ||
const std::vector< std::string > & | regexp | ||
) |
Definition at line 301 of file TagStates.cc.
References ERROR_UNHANDLED_EXCEPTION, Diades::Automata::Experimental::faFromDescriptor(), Diades::Automata::Experimental::faToDdAutFile(), Diades::CmdInterface::printCommandLineError(), Diades::Automata::Experimental::DdAutFileDescriptor::readStream(), and tagStates().
Referenced by tagDdAutStates().
void tagPredecessors | ( | DdAutFA & | fa, |
std::list< DdAutFA::State > & | acceptors, | ||
CstStMap< char > & | mapping | ||
) |
Definition at line 237 of file TagStates.cc.
References applyTag(), current, Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::inputTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::inputTransitionEnd(), and prefixclosedfinal.
Referenced by setPrefixClosedAcceptorTag().
void tagStates | ( | DdAutFA & | fa, |
DdAutStateManager & | sManager, | ||
const std::string & | expr | ||
) |
Definition at line 270 of file TagStates.cc.
References applyTag(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::getState(), prefixclosedfinal, setPrefixClosedAcceptorTag(), Diades::Automata::Experimental::StatePropertyManager< _StateProperty, _StatePropertyId, NullStProperty, NullStPropertyId, Hash >::statePropertyId(), and Diades::Utils::InfoManager< _Info, _InfoId, _NullInfo, _NullInfoId, _Hash >::storage().
Referenced by tagDdAutStates2().
const string detailedcomment |
Definition at line 76 of file TagStates.cc.
Referenced by main().
FileSuffixes suffixes({"ddaut"}) |
Referenced by tagDdAutStates().
const std::unordered_map<std::string,Tag> tagOf |
Definition at line 163 of file TagStates.cc.