diff --git a/alib2algo/src/automaton/properties/BackwardBisimulation.cpp b/alib2algo/src/automaton/properties/BackwardBisimulation.cpp index 5f82105558a0585d90c65b00c39f4f609872e8d3..0139fe58d095eed2bf1fb94ecbcce99a67fa5fea 100644 --- a/alib2algo/src/automaton/properties/BackwardBisimulation.cpp +++ b/alib2algo/src/automaton/properties/BackwardBisimulation.cpp @@ -10,6 +10,18 @@ namespace { +auto BackwardBisimulationDFA = registration::AbstractRegister < automaton::properties::BackwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFA < > & > ( automaton::properties::BackwardBisimulation::backwardBisimulation, "fta" ).setDocumentation ( +"Computes a relation on states of the DFA satisfying the backward bisimulation definition.\n\ +\n\ +@param fta the examined automaton.\n\ +@return set of pairs of states of the @p fta that are the backward bisimulation." ); + +auto BackwardBisimulationNFA = registration::AbstractRegister < automaton::properties::BackwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::NFA < > & > ( automaton::properties::BackwardBisimulation::backwardBisimulation, "fta" ).setDocumentation ( +"Computes a relation on states of the NFA satisfying the backward bisimulation definition.\n\ +\n\ +@param fta the examined automaton.\n\ +@return set of pairs of states of the @p fta that are the backward bisimulation." ); + auto BackwardBisimulationDFTA = registration::AbstractRegister < automaton::properties::BackwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFTA < > & > ( automaton::properties::BackwardBisimulation::backwardBisimulation, "fta" ).setDocumentation ( "Computes a relation on states of the DFTA satisfying the backward bisimulation definition.\n\ \n\ diff --git a/alib2algo/src/automaton/properties/BackwardBisimulation.h b/alib2algo/src/automaton/properties/BackwardBisimulation.h index 1fdca25c6f1e6ba828ceaf18e64210ac793bfc86..a19650651d116a26d70d6363cb3a4dc15dc81896 100644 --- a/alib2algo/src/automaton/properties/BackwardBisimulation.h +++ b/alib2algo/src/automaton/properties/BackwardBisimulation.h @@ -30,6 +30,9 @@ #include <automaton/TA/DFTA.h> #include <automaton/TA/NFTA.h> +#include <automaton/FSM/DFA.h> +#include <automaton/FSM/NFA.h> + namespace automaton { namespace properties { @@ -40,13 +43,15 @@ namespace properties { */ class BackwardBisimulation { template < class StateType > - static ext::set < ext::pair < StateType, StateType > > initial ( const ext::set < StateType > & states ) { + static ext::set < ext::pair < StateType, StateType > > initial ( const ext::set < StateType > & states, const ext::set < StateType > & initials ) { ext::set < ext::pair < StateType, StateType > > init; for ( const StateType & a : states ) { for ( const StateType & b : states ) { - init.insert ( ext::make_pair ( a, b ) ); - init.insert ( ext::make_pair ( b, a ) ); + if ( initials.count ( a ) == initials.count ( b ) ) { + init.insert ( ext::make_pair ( a, b ) ); + init.insert ( ext::make_pair ( b, a ) ); + } } } @@ -54,6 +59,26 @@ class BackwardBisimulation { } public: + /** + * Computes a relation on states of the DFA satisfying the backward bisimulation definition. + * + * @param fta the examined automaton + * + * @return set of pairs of states of the @p fta that are the backward bisimulation. + */ + template < class SymbolType, class StateType > + static ext::set < ext::pair < StateType, StateType > > backwardBisimulation ( const automaton::DFA < SymbolType, StateType > & fta ); + + /** + * Computes a relation on states of the NFA satisfying the backward bisimulation definition. + * + * @param fta the examined automaton + * + * @return set of pairs of states of the @p fta that are the backward bisimulation. + */ + template < class SymbolType, class StateType > + static ext::set < ext::pair < StateType, StateType > > backwardBisimulation ( const automaton::NFA < SymbolType, StateType > & fta ); + /** * Computes a relation on states of the DFTA satisfying the backward bisimulation definition. * @@ -75,6 +100,51 @@ public: static ext::set < ext::pair < StateType, StateType > > backwardBisimulation ( const automaton::NFTA < SymbolType, StateType > & fta ); }; +template < class SymbolType, class StateType > +ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBisimulation ( const automaton::DFA < SymbolType, StateType > & fta ) { + return backwardBisimulation ( NFA < SymbolType, StateType > ( fta ) ); +} + +template < class SymbolType, class StateType > +ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBisimulation ( const automaton::NFA < SymbolType, StateType > & fta ) { + ext::set < ext::pair < StateType, StateType > > backwardBisimulation = initial ( fta.getStates ( ), { fta.getInitialState ( ) } ); + + bool changed; + do { + changed = false; + + for ( const StateType & p : fta.getStates ( ) ) { + for ( const StateType & q : fta.getStates ( ) ) { + if ( ! backwardBisimulation.contains ( ext::make_pair ( p, q ) ) ) + continue; + + for ( const std::pair < const ext::pair < SymbolType, StateType >, StateType > & pTransition : fta.getTransitionsToState ( p ) ) { + + bool exists = false; + for ( const std::pair < const ext::pair < SymbolType, StateType >, StateType > & qTransition : fta.getTransitionsToState ( q ) ) { + if ( qTransition.first.first != pTransition.first.first ) + continue; + + if ( backwardBisimulation.contains ( ext::make_pair ( pTransition.first.second, qTransition.first.second) ) ) { + exists = true; + break; + } + } + + if ( ! exists ) { + backwardBisimulation.erase ( ext::make_pair ( p, q ) ); + backwardBisimulation.erase ( ext::make_pair ( q, p ) ); + changed = true; + break; + } + } + } + } + } while ( changed ); + + return backwardBisimulation; +} + template < class SymbolType, class StateType > ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBisimulation ( const automaton::DFTA < SymbolType, StateType > & fta ) { return backwardBisimulation ( NFTA < SymbolType, StateType > ( fta ) ); @@ -82,7 +152,7 @@ ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBi template < class SymbolType, class StateType > ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBisimulation ( const automaton::NFTA < SymbolType, StateType > & fta ) { - ext::set < ext::pair < StateType, StateType > > backwardBisimulation = initial ( fta.getStates ( ) ); + ext::set < ext::pair < StateType, StateType > > backwardBisimulation = initial ( fta.getStates ( ), { } ); bool changed; do { diff --git a/alib2algo/src/automaton/properties/ForwardBisimulation.cpp b/alib2algo/src/automaton/properties/ForwardBisimulation.cpp index b800f32a1028f100186de9d2c7147c726e68d981..2ac86db876f8e81a36961b11ea02d1b66eccd3a8 100644 --- a/alib2algo/src/automaton/properties/ForwardBisimulation.cpp +++ b/alib2algo/src/automaton/properties/ForwardBisimulation.cpp @@ -10,6 +10,18 @@ namespace { +auto ForwardBisimulationNFA = registration::AbstractRegister < automaton::properties::ForwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::NFA < > & > ( automaton::properties::ForwardBisimulation::forwardBisimulation, "fta" ).setDocumentation ( +"Computes a relation on states of the NFA satisfying the forward bisimulation definition.\n\ +\n\ +@param fta the examined automaton.\n\ +@return set of pairs of states of the @p fta that are the forward bisimulation." ); + +auto ForwardBisimulationDFA = registration::AbstractRegister < automaton::properties::ForwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFA < > & > ( automaton::properties::ForwardBisimulation::forwardBisimulation, "fta" ).setDocumentation ( +"Computes a relation on states of the DFA satisfying the forward bisimulation definition.\n\ +\n\ +@param fta the examined automaton.\n\ +@return set of pairs of states of the @p fta that are the forward bisimulation." ); + auto ForwardBisimulationNFTA = registration::AbstractRegister < automaton::properties::ForwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::NFTA < > & > ( automaton::properties::ForwardBisimulation::forwardBisimulation, "fta" ).setDocumentation ( "Computes a relation on states of the NFTA satisfying the forward bisimulation definition.\n\ \n\ diff --git a/alib2algo/src/automaton/properties/ForwardBisimulation.h b/alib2algo/src/automaton/properties/ForwardBisimulation.h index e16cd7b2241828a049967c34cb74e70f1d3d05bb..ccde55cef627ed4e160f0ad7e4250de78fc71685 100644 --- a/alib2algo/src/automaton/properties/ForwardBisimulation.h +++ b/alib2algo/src/automaton/properties/ForwardBisimulation.h @@ -30,6 +30,9 @@ #include <automaton/TA/DFTA.h> #include <automaton/TA/NFTA.h> +#include <automaton/FSM/DFA.h> +#include <automaton/FSM/NFA.h> + namespace automaton { namespace properties { @@ -56,6 +59,27 @@ class ForwardBisimulation { } public: + + /** + * Computes a relation on states of the DFA satisfying the forward bisimulation definition. + * + * @param fta the examined automaton + * + * @return set of pairs of states of the @p fta that are the forward bisimulation. + */ + template < class SymbolType, class StateType > + static ext::set < ext::pair < StateType, StateType > > forwardBisimulation ( const automaton::DFA < SymbolType, StateType > & fta ); + + /** + * Computes a relation on states of the NFA satisfying the forward bisimulation definition. + * + * @param fta the examined automaton + * + * @return set of pairs of states of the @p fta that are the forward bisimulation. + */ + template < class SymbolType, class StateType > + static ext::set < ext::pair < StateType, StateType > > forwardBisimulation ( const automaton::NFA < SymbolType, StateType > & fta ); + /** * Computes a relation on states of the DFTA satisfying the forward bisimulation definition. * @@ -77,6 +101,42 @@ public: static ext::set < ext::pair < StateType, StateType > > forwardBisimulation ( const automaton::NFTA < SymbolType, StateType > & fta ); }; +template < class SymbolType, class StateType > +ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisimulation ( const automaton::DFA < SymbolType, StateType > & fta ) { + return forwardBisimulation ( automaton::NFA < SymbolType, StateType > ( fta ) ); +} + +template < class SymbolType, class StateType > +ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisimulation ( const automaton::NFA < SymbolType, StateType > & fta ) { + ext::set < ext::pair < StateType, StateType > > forwardBisimulation = initial ( fta.getStates ( ), fta.getFinalStates ( ) ); + + bool changed; + do { + changed = false; + + for ( const StateType & p : fta.getStates ( ) ) { + for ( const StateType & q : fta.getStates ( ) ) { + if ( ! forwardBisimulation.contains ( ext::make_pair ( p, q ) ) ) + continue; + + for ( const std::pair < const ext::pair < SymbolType, StateType >, StateType > & transition : fta.getTransitions ( ) ) { + if ( transition.first.second == p ) { + const auto & transition2 = fta.getTransitions ( ).find ( std::make_pair ( transition.first.first, q ) ); + + if ( transition2 == fta.getTransitions ( ).end ( ) || ! forwardBisimulation.contains ( ext::make_pair ( transition.second, transition2->second ) ) ) { + forwardBisimulation.erase ( ext::make_pair ( p, q ) ); + forwardBisimulation.erase ( ext::make_pair ( q, p ) ); + changed = true; + } + } + } + } + } + } while ( changed ); + + return forwardBisimulation; +} + template < class SymbolType, class StateType > ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisimulation ( const automaton::DFTA < SymbolType, StateType > & fta ) { return forwardBisimulation ( automaton::NFTA < SymbolType, StateType > ( fta ) );