From 302a4980e6935c28025cd13890ce1b61df88a2aa Mon Sep 17 00:00:00 2001
From: Jan Travnicek <jan.travnicek@.fit.cvut.cz>
Date: Wed, 2 Oct 2019 15:56:05 +0200
Subject: [PATCH] backward bisimulation and forward bisimulation by definition
---
.../properties/BackwardBisimulation.cpp | 25 ++++
.../properties/BackwardBisimulation.h | 133 ++++++++++++++++++
.../properties/ForwardBisimulation.cpp | 25 ++++
.../properties/ForwardBisimulation.h | 125 ++++++++++++++++
examples2/automaton/NFTA_fab_faa.xml | 95 +++++++++++++
5 files changed, 403 insertions(+)
create mode 100644 alib2algo/src/automaton/properties/BackwardBisimulation.cpp
create mode 100644 alib2algo/src/automaton/properties/BackwardBisimulation.h
create mode 100644 alib2algo/src/automaton/properties/ForwardBisimulation.cpp
create mode 100644 alib2algo/src/automaton/properties/ForwardBisimulation.h
create mode 100644 examples2/automaton/NFTA_fab_faa.xml
diff --git a/alib2algo/src/automaton/properties/BackwardBisimulation.cpp b/alib2algo/src/automaton/properties/BackwardBisimulation.cpp
new file mode 100644
index 0000000000..5f82105558
--- /dev/null
+++ b/alib2algo/src/automaton/properties/BackwardBisimulation.cpp
@@ -0,0 +1,25 @@
+/*
+* BackwardBisimulation.cpp
+ *
+ * Created on: 27. 3. 2019
+ * Author: Tomas Pecka
+ */
+
+#include "BackwardBisimulation.h"
+#include <registration/AlgoRegistration.hpp>
+
+namespace {
+
+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\
+@param fta the examined automaton.\n\
+@return set of pairs of states of the @p fta that are the backward bisimulation." );
+
+auto BackwardBisimulationNFTA = registration::AbstractRegister < automaton::properties::BackwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::NFTA < > & > ( automaton::properties::BackwardBisimulation::backwardBisimulation, "fta" ).setDocumentation (
+"Computes a relation on states of the NFTA 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
new file mode 100644
index 0000000000..1fdca25c6f
--- /dev/null
+++ b/alib2algo/src/automaton/properties/BackwardBisimulation.h
@@ -0,0 +1,133 @@
+/*
+ * BackwardBisimulation.h
+ *
+ * This file is part of Algorithms library toolkit.
+ * Copyright (C) 2017 Jan Travnicek (jan.travnicek@fit.cvut.cz)
+
+ * Algorithms library toolkit is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+
+ * Algorithms library toolkit is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+
+ * You should have received a copy of the GNU General Public License
+ * along with Algorithms library toolkit. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Created on: 27. 3. 2019
+ * Author: Tomas Pecka
+ */
+
+#ifndef BACKWARD_BISIMULATION_H_
+#define BACKWARD_BISIMULATION_H_
+
+#include <alib/set>
+#include <alib/map>
+
+#include <automaton/TA/DFTA.h>
+#include <automaton/TA/NFTA.h>
+
+namespace automaton {
+
+namespace properties {
+
+/**
+ * Find all backwardBisimulation pairs of states of DFA.
+ * Implements table-filling algorithm, Hopcroft 2nd edition, 4.4.1
+ */
+class BackwardBisimulation {
+ template < class StateType >
+ static ext::set < ext::pair < StateType, StateType > > initial ( const ext::set < StateType > & states ) {
+ 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 ) );
+ }
+ }
+
+ return init;
+ }
+
+public:
+ /**
+ * 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::DFTA < 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::NFTA < SymbolType, StateType > & fta );
+};
+
+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 ) );
+}
+
+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 ( ) );
+
+ 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::vector < StateType > >, StateType > & pTransition : fta.getTransitionsToState ( p ) ) {
+
+ bool exists = false;
+ for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::vector < StateType > >, StateType > & qTransition : fta.getTransitionsToState ( q ) ) {
+ if ( qTransition.first.first != pTransition.first.first )
+ continue;
+
+ size_t inRelation = 0;
+ for ( size_t i = 0; i < pTransition.first.second.size ( ); ++ i ) {
+ if ( backwardBisimulation.contains ( ext::make_pair ( pTransition.first.second [ i ], qTransition.first.second [ i ] ) ) )
+ ++ inRelation;
+ }
+
+ if ( inRelation == pTransition.first.second.size ( ) ) {
+ 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 */
+
+#endif /* BACKWARD_BISIMULATION_H_ */
diff --git a/alib2algo/src/automaton/properties/ForwardBisimulation.cpp b/alib2algo/src/automaton/properties/ForwardBisimulation.cpp
new file mode 100644
index 0000000000..b800f32a10
--- /dev/null
+++ b/alib2algo/src/automaton/properties/ForwardBisimulation.cpp
@@ -0,0 +1,25 @@
+/*
+* ForwardBisimulation.cpp
+ *
+ * Created on: 27. 3. 2019
+ * Author: Tomas Pecka
+ */
+
+#include "ForwardBisimulation.h"
+#include <registration/AlgoRegistration.hpp>
+
+namespace {
+
+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\
+@param fta the examined automaton.\n\
+@return set of pairs of states of the @p fta that are the forward bisimulation." );
+
+auto ForwardBisimulationDFTA = registration::AbstractRegister < automaton::properties::ForwardBisimulation, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFTA < > & > ( automaton::properties::ForwardBisimulation::forwardBisimulation, "fta" ).setDocumentation (
+"Computes a relation on states of the 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
new file mode 100644
index 0000000000..e16cd7b224
--- /dev/null
+++ b/alib2algo/src/automaton/properties/ForwardBisimulation.h
@@ -0,0 +1,125 @@
+/*
+ * ForwardBisimulation.h
+ *
+ * This file is part of Algorithms library toolkit.
+ * Copyright (C) 2017 Jan Travnicek (jan.travnicek@fit.cvut.cz)
+
+ * Algorithms library toolkit is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+
+ * Algorithms library toolkit is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+
+ * You should have received a copy of the GNU General Public License
+ * along with Algorithms library toolkit. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Created on: 27. 3. 2019
+ * Author: Tomas Pecka
+ */
+
+#ifndef FORWARD_BISIMULATION_H_
+#define FORWARD_BISIMULATION_H_
+
+#include <alib/set>
+#include <alib/map>
+
+#include <automaton/TA/DFTA.h>
+#include <automaton/TA/NFTA.h>
+
+namespace automaton {
+
+namespace properties {
+
+/**
+ * Find all forwardBisimulation pairs of states of DFA.
+ * Implements table-filling algorithm, Hopcroft 2nd edition, 4.4.1
+ */
+class ForwardBisimulation {
+ template < class StateType >
+ static ext::set < ext::pair < StateType, StateType > > initial ( const ext::set < StateType > & states, const ext::set < StateType > & finals ) {
+ ext::set < ext::pair < StateType, StateType > > init;
+
+ for ( const StateType & a : states ) {
+ for ( const StateType & b : states ) {
+ if ( finals.count ( a ) == finals.count ( b ) ) {
+ init.insert ( ext::make_pair ( a, b ) );
+ init.insert ( ext::make_pair ( b, a ) );
+ }
+ }
+ }
+
+ return init;
+ }
+
+public:
+ /**
+ * 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::DFTA < 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::NFTA < SymbolType, StateType > & fta );
+};
+
+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 ) );
+}
+
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisimulation ( const automaton::NFTA < 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::vector < StateType > >, StateType > & transition : fta.getTransitions ( ) ) {
+ for ( size_t i = 0; i < transition.first.second.size ( ); ++ i ) {
+ if ( transition.first.second [ i ] == p ) {
+ ext::vector < StateType > copy = transition.first.second;
+ copy [ i ] = q;
+
+ const auto & transition2 = fta.getTransitions ( ).find ( std::make_pair ( transition.first.first, std::move ( copy ) ) );
+
+ 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;
+}
+
+} /* namespace properties */
+
+} /* namespace automaton */
+
+#endif /* FORWARD_BISIMULATION_H_ */
diff --git a/examples2/automaton/NFTA_fab_faa.xml b/examples2/automaton/NFTA_fab_faa.xml
new file mode 100644
index 0000000000..8ecae02e1b
--- /dev/null
+++ b/examples2/automaton/NFTA_fab_faa.xml
@@ -0,0 +1,95 @@
+<?xml version="1.0"?>
+<NFTA>
+ <states>
+ <String>1</String>
+ <String>2</String>
+ <String>3</String>
+ <String>4</String>
+ <String>5</String>
+ <String>6</String>
+ </states>
+ <rankedInputAlphabet>
+ <RankedSymbol>
+ <String>f</String>
+ <UnsignedLong>2</UnsignedLong>
+ </RankedSymbol>
+ <RankedSymbol>
+ <String>a</String>
+ <UnsignedLong>0</UnsignedLong>
+ </RankedSymbol>
+ <RankedSymbol>
+ <String>b</String>
+ <UnsignedLong>0</UnsignedLong>
+ </RankedSymbol>
+ </rankedInputAlphabet>
+ <finalStates>
+ <String>3</String>
+ <String>6</String>
+ </finalStates>
+ <transitions>
+ <transition>
+ <input>
+ <RankedSymbol><String>a</String><UnsignedLong>0</UnsignedLong></RankedSymbol>
+ </input>
+ <from>
+ </from>
+ <to>
+ <String>1</String>
+ </to>
+ </transition>
+ <transition>
+ <input>
+ <RankedSymbol><String>a</String><UnsignedLong>0</UnsignedLong></RankedSymbol>
+ </input>
+ <from>
+ </from>
+ <to>
+ <String>4</String>
+ </to>
+ </transition>
+ <transition>
+ <input>
+ <RankedSymbol><String>a</String><UnsignedLong>0</UnsignedLong></RankedSymbol>
+ </input>
+ <from>
+ </from>
+ <to>
+ <String>5</String>
+ </to>
+ </transition>
+ <transition>
+ <input>
+ <RankedSymbol><String>b</String><UnsignedLong>0</UnsignedLong></RankedSymbol>
+ </input>
+ <from>
+ </from>
+ <to>
+ <String>2</String>
+ </to>
+ </transition>
+ <transition>
+ <input>
+ <RankedSymbol><String>f</String><UnsignedLong>2</UnsignedLong></RankedSymbol>
+ </input>
+ <from>
+ <String>1</String>
+ <String>2</String>
+ </from>
+ <to>
+ <String>3</String>
+ </to>
+ </transition>
+ <transition>
+ <input>
+ <RankedSymbol><String>f</String><UnsignedLong>2</UnsignedLong></RankedSymbol>
+ </input>
+ <from>
+ <String>4</String>
+ <String>5</String>
+ </from>
+ <to>
+ <String>6</String>
+ </to>
+ </transition>
+ </transitions>
+</NFTA>
--
GitLab