From ebde3b29bad65253801426b6713c33a60c19292b Mon Sep 17 00:00:00 2001
From: Jan Travnicek <jan.travnicek@.fit.cvut.cz>
Date: Mon, 3 Feb 2020 15:49:23 +0100
Subject: [PATCH] unranked tree automata bisimulation
---
.../properties/BackwardBisimulation.cpp | 12 +++
.../properties/BackwardBisimulation.h | 80 +++++++++++++++++++
.../properties/DistinguishableStates.cpp | 6 ++
.../properties/DistinguishableStates.h | 44 ++++++++++
.../properties/ForwardBisimulation.cpp | 12 +++
.../properties/ForwardBisimulation.h | 69 ++++++++++++++++
6 files changed, 223 insertions(+)
diff --git a/alib2algo/src/automaton/properties/BackwardBisimulation.cpp b/alib2algo/src/automaton/properties/BackwardBisimulation.cpp
index 0139fe58d0..51d1385a4a 100644
--- a/alib2algo/src/automaton/properties/BackwardBisimulation.cpp
+++ b/alib2algo/src/automaton/properties/BackwardBisimulation.cpp
@@ -34,4 +34,16 @@ auto BackwardBisimulationNFTA = registration::AbstractRegister < automaton::prop
@param fta the examined automaton.\n\
@return set of pairs of states of the @p fta that are the backward bisimulation." );
+auto BackwardBisimulationUnorderedDFTA = registration::AbstractRegister < automaton::properties::BackwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::UnorderedDFTA < > & > ( automaton::properties::BackwardBisimulation::backwardBisimulation, "fta" ).setDocumentation (
+"Computes a relation on states of the UnorderedDFTA 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 BackwardBisimulationUnorderedNFTA = registration::AbstractRegister < automaton::properties::BackwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::UnorderedNFTA < > & > ( automaton::properties::BackwardBisimulation::backwardBisimulation, "fta" ).setDocumentation (
+"Computes a relation on states of the UnorderedNFTA 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." );
+
} /* namespace */
diff --git a/alib2algo/src/automaton/properties/BackwardBisimulation.h b/alib2algo/src/automaton/properties/BackwardBisimulation.h
index 9215c55e07..c8c1745384 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/TA/UnorderedDFTA.h>
+#include <automaton/TA/UnorderedNFTA.h>
+
#include <automaton/FSM/DFA.h>
#include <automaton/FSM/NFA.h>
@@ -98,6 +101,26 @@ public:
*/
template < class SymbolType, class StateType >
static ext::set < ext::pair < StateType, StateType > > backwardBisimulation ( const automaton::NFTA < SymbolType, StateType > & fta );
+
+ /**
+ * Computes a relation on states of the DFTA 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::UnorderedDFTA < SymbolType, StateType > & fta );
+
+ /**
+ * Computes a relation on states of the NFTA 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::UnorderedNFTA < SymbolType, StateType > & fta );
};
template < class SymbolType, class StateType >
@@ -196,6 +219,63 @@ ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBi
return backwardBisimulation;
}
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBisimulation ( const automaton::UnorderedDFTA < SymbolType, StateType > & fta ) {
+ return backwardBisimulation ( UnorderedNFTA < SymbolType, StateType > ( fta ) );
+}
+
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBisimulation ( const automaton::UnorderedNFTA < SymbolType, StateType > & fta ) {
+ ext::set < ext::pair < StateType, StateType > > backwardBisimulation = initial ( fta.getStates ( ), { } );
+
+ 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 < common::ranked_symbol < SymbolType >, ext::multiset < StateType > >, StateType > & pTransition : fta.getTransitionsToState ( p ) ) {
+
+ ext::multiset < StateType > pSource;
+ for ( const StateType & state : pTransition.first.second ) {
+ auto lower = backwardBisimulation.lower_bound ( ext::slice_comp ( state ) );
+ pSource.insert ( lower->second );
+ }
+
+ bool exists = false;
+ for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::multiset < StateType > >, StateType > & qTransition : fta.getTransitionsToState ( q ) ) {
+ if ( qTransition.first.first != pTransition.first.first )
+ continue;
+
+ ext::multiset < StateType > qSource;
+ for ( const StateType & state : qTransition.first.second ) {
+ auto lower = backwardBisimulation.lower_bound ( ext::slice_comp ( state ) );
+ qSource.insert ( lower->second );
+ }
+
+ if ( pSource == qSource ) {
+ 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;
+}
+
} /* namespace properties */
} /* namespace automaton */
diff --git a/alib2algo/src/automaton/properties/DistinguishableStates.cpp b/alib2algo/src/automaton/properties/DistinguishableStates.cpp
index e161aaf38c..43910bd8d2 100644
--- a/alib2algo/src/automaton/properties/DistinguishableStates.cpp
+++ b/alib2algo/src/automaton/properties/DistinguishableStates.cpp
@@ -22,4 +22,10 @@ auto DistinguishableStatesDFTA = registration::AbstractRegister < automaton::pro
@param dfta finite tree automaton.\n\
@return set of pairs of distinguishable states" );
+auto DistinguishableStatesUnorderedDFTA = registration::AbstractRegister < automaton::properties::DistinguishableStates, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::UnorderedDFTA < > & > ( automaton::properties::DistinguishableStates::distinguishable, "fta" ).setDocumentation (
+"Computes the pairs of distinguishable states in given UnorderedDFTA.\n\
+\n\
+@param unordered dfta finite tree automaton.\n\
+@return set of pairs of distinguishable states" );
+
} /* namespace */
diff --git a/alib2algo/src/automaton/properties/DistinguishableStates.h b/alib2algo/src/automaton/properties/DistinguishableStates.h
index 0de068158c..fc01074ae0 100644
--- a/alib2algo/src/automaton/properties/DistinguishableStates.h
+++ b/alib2algo/src/automaton/properties/DistinguishableStates.h
@@ -30,6 +30,8 @@
#include <automaton/FSM/DFA.h>
#include <automaton/TA/DFTA.h>
+#include <automaton/TA/UnorderedDFTA.h>
+
namespace automaton {
namespace properties {
@@ -69,6 +71,9 @@ public:
template < class SymbolType, class StateType >
static ext::set < ext::pair < StateType, StateType > > distinguishable ( const automaton::DFTA < SymbolType, StateType > & fta );
+
+ template < class SymbolType, class StateType >
+ static ext::set < ext::pair < StateType, StateType > > distinguishable ( const automaton::UnorderedDFTA < SymbolType, StateType > & fta );
};
template < class SymbolType, class StateType >
@@ -144,6 +149,45 @@ ext::set < ext::pair < StateType, StateType > > DistinguishableStates::distingui
return distinguishable;
}
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > DistinguishableStates::distinguishable ( const automaton::UnorderedDFTA < SymbolType, StateType > & fta ) {
+ ext::set < ext::pair < StateType, StateType > > distinguishable = initial ( fta.getStates ( ), fta.getFinalStates ( ) );
+
+ bool changed;
+ do {
+ changed = false;
+
+ for ( const StateType & a : fta.getStates ( ) ) {
+ for ( const StateType & b : fta.getStates ( ) ) {
+ if ( distinguishable.count ( ext::make_pair ( a, b ) ) )
+ continue;
+
+ for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::multiset < StateType > >, StateType > & transition : fta.getTransitions ( ) ) {
+ for ( const StateType & state : transition.first.second ) {
+ if ( state == a ) {
+ ext::multiset < StateType > copy = transition.first.second;
+ copy.erase ( copy.find ( state ) );
+ copy.insert ( b );
+
+ const auto & transition2 = fta.getTransitions ( ).find ( std::make_pair ( transition.first.first, std::move ( copy ) ) );
+
+ if ( transition2 == fta.getTransitions ( ).end ( ) || distinguishable.count ( ext::make_pair ( transition.second, transition2->second ) ) ) {
+ // end up in dead state - dead state is be distinguishable from every other state OR
+ // end up in distinguishable states
+ distinguishable.insert ( ext::make_pair ( a, b ) );
+ distinguishable.insert ( ext::make_pair ( b, a ) );
+ changed = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ } while ( changed );
+
+ return distinguishable;
+}
+
} /* namespace properties */
} /* namespace automaton */
diff --git a/alib2algo/src/automaton/properties/ForwardBisimulation.cpp b/alib2algo/src/automaton/properties/ForwardBisimulation.cpp
index 2ac86db876..de0566955c 100644
--- a/alib2algo/src/automaton/properties/ForwardBisimulation.cpp
+++ b/alib2algo/src/automaton/properties/ForwardBisimulation.cpp
@@ -34,4 +34,16 @@ auto ForwardBisimulationDFTA = registration::AbstractRegister < automaton::prope
@param fta the examined automaton.\n\
@return set of pairs of states of the @p fta that are the forward bisimulation." );
+auto ForwardBisimulationUnorderedNFTA = registration::AbstractRegister < automaton::properties::ForwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::UnorderedNFTA < > & > ( automaton::properties::ForwardBisimulation::forwardBisimulation, "fta" ).setDocumentation (
+"Computes a relation on states of the Unordered NFTA 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 ForwardBisimulationUnorderedDFTA = registration::AbstractRegister < automaton::properties::ForwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::UnorderedDFTA < > & > ( automaton::properties::ForwardBisimulation::forwardBisimulation, "fta" ).setDocumentation (
+"Computes a relation on states of the Unordered DFTA 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." );
+
} /* namespace */
diff --git a/alib2algo/src/automaton/properties/ForwardBisimulation.h b/alib2algo/src/automaton/properties/ForwardBisimulation.h
index 963b37081d..74a4523041 100644
--- a/alib2algo/src/automaton/properties/ForwardBisimulation.h
+++ b/alib2algo/src/automaton/properties/ForwardBisimulation.h
@@ -29,6 +29,7 @@
#include <automaton/TA/DFTA.h>
#include <automaton/TA/NFTA.h>
+#include <automaton/TA/UnorderedNFTA.h>
#include <automaton/FSM/DFA.h>
#include <automaton/FSM/NFA.h>
@@ -99,6 +100,26 @@ public:
*/
template < class SymbolType, class StateType >
static ext::set < ext::pair < StateType, StateType > > forwardBisimulation ( const automaton::NFTA < SymbolType, StateType > & fta );
+
+ /**
+ * Computes a relation on states of the DFTA 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::UnorderedDFTA < SymbolType, StateType > & fta );
+
+ /**
+ * Computes a relation on states of the NFTA 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::UnorderedNFTA < SymbolType, StateType > & fta );
};
template < class SymbolType, class StateType >
@@ -190,6 +211,54 @@ ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisi
return forwardBisimulation;
}
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisimulation ( const automaton::UnorderedDFTA < SymbolType, StateType > & fta ) {
+ return forwardBisimulation ( automaton::UnorderedNFTA < SymbolType, StateType > ( fta ) );
+}
+
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisimulation ( const automaton::UnorderedNFTA < 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 < common::ranked_symbol < SymbolType >, ext::multiset < StateType > >, StateType > & pTransition : fta.getTransitions ( ) ) {
+ for ( const StateType & state : pTransition.first.second ) {
+ if ( state == p ) {
+ ext::multiset < StateType > copy = pTransition.first.second;
+ copy.erase ( copy.find ( state ) );
+ copy.insert ( q );
+
+ bool exists = false;
+ for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::multiset < StateType > >, StateType > & qTransition : fta.getTransitions ( ).equal_range ( std::make_pair ( pTransition.first.first, std::move ( copy ) ) ) ) {
+ if ( forwardBisimulation.contains ( ext::make_pair ( pTransition.second, qTransition.second ) ) ) {
+ exists = true;
+ break;
+ }
+ }
+
+ if ( ! exists ) {
+ forwardBisimulation.erase ( ext::make_pair ( p, q ) );
+ forwardBisimulation.erase ( ext::make_pair ( q, p ) );
+ changed = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ } while ( changed );
+
+ return forwardBisimulation;
+}
+
} /* namespace properties */
} /* namespace automaton */
--
GitLab