From df4f38bee1bd959fd2f673a5fb9793212d8e561a Mon Sep 17 00:00:00 2001
From: Tomas Pecka <peckato1@fit.cvut.cz>
Date: Wed, 27 Mar 2019 10:57:29 +0100
Subject: [PATCH] Algo: Distinguishable states of DFA

---
 .../properties/DistinguishableStates.cpp      |  24 ++++
 .../properties/DistinguishableStates.h        | 103 ++++++++++++++++++
 .../properties/DistinguishableStatesTest.cpp  |  97 +++++++++++++++++
 3 files changed, 224 insertions(+)
 create mode 100644 alib2algo/src/automaton/properties/DistinguishableStates.cpp
 create mode 100644 alib2algo/src/automaton/properties/DistinguishableStates.h
 create mode 100644 alib2algo/test-src/automaton/properties/DistinguishableStatesTest.cpp

diff --git a/alib2algo/src/automaton/properties/DistinguishableStates.cpp b/alib2algo/src/automaton/properties/DistinguishableStates.cpp
new file mode 100644
index 0000000000..7997a70f39
--- /dev/null
+++ b/alib2algo/src/automaton/properties/DistinguishableStates.cpp
@@ -0,0 +1,24 @@
+/*
+* DistinguishableStates.cpp
+ *
+ *  Created on: 27. 3. 2019
+ *	  Author: Tomas Pecka
+ */
+
+#include "DistinguishableStates.h"
+#include <registration/AlgoRegistration.hpp>
+
+namespace automaton {
+
+namespace properties {
+
+auto DistinguishableStatesDFA = registration::AbstractRegister < DistinguishableStates, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFA < > & > ( DistinguishableStates::distinguishableStates, "fsm" ).setDocumentation (
+"Computes the pairs of distinguishable states in given DFA.\n\
+\n\
+@param dfa finite automaton.\n\
+@return set of pairs of distinguishable states" );
+
+} /* namespace properties */
+
+} /* namespace automaton */
+
diff --git a/alib2algo/src/automaton/properties/DistinguishableStates.h b/alib2algo/src/automaton/properties/DistinguishableStates.h
new file mode 100644
index 0000000000..09270d7704
--- /dev/null
+++ b/alib2algo/src/automaton/properties/DistinguishableStates.h
@@ -0,0 +1,103 @@
+/*
+ * DistinguishableStates.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 DISTINGUISHABLE_STATES_H_
+#define DISTINGUISHABLE_STATES_H_
+
+#include <alib/set>
+#include <alib/map>
+
+#include <automaton/FSM/DFA.h>
+
+#include <automaton/Automaton.h>
+
+namespace automaton {
+
+namespace properties {
+
+/**
+ * Find all distinguishable pairs of states of DFA.
+ * Implements table-filling algorithm, Hopcroft 2nd edition, 4.4.1
+ */
+class DistinguishableStates {
+public:
+	/**
+	 * Find all distinguishable pairs of states of DFA.
+	 * Implements table-filling algorithm, Hopcroft 2nd edition, 4.4.1
+	 * O(n^4) version. TODO quadratic-time version.
+	 *
+	 * @param fsm automaton
+	 * @return set of pairs of distinguishable states of @p fsm
+	 */
+	template < class SymbolType, class StateType >
+	static ext::set < ext::pair < StateType, StateType > > distinguishableStates ( const automaton::DFA < SymbolType, StateType > & fsm );
+};
+
+template < class SymbolType, class StateType >
+ext::set < ext::pair < StateType, StateType > > DistinguishableStates::distinguishableStates ( const automaton::DFA < SymbolType, StateType > & fsm ) {
+	ext::set < ext::pair < StateType, StateType > > distinguishable;
+
+	for ( const StateType & a : fsm.getStates ( ) ) {
+		for ( const StateType & b : fsm.getStates ( ) ) {
+			if ( ( fsm.getFinalStates ( ).count ( a ) == 0 ) ^ ( fsm.getFinalStates ( ).count ( b ) == 0 ) ) {
+				distinguishable.insert ( ext::make_pair ( a, b ) );
+				distinguishable.insert ( ext::make_pair ( b, a ) );
+			}
+		}
+	}
+
+	bool changed;
+	do {
+		changed = false;
+
+		for ( const StateType & a : fsm.getStates ( ) ) {
+			for ( const StateType & b : fsm.getStates ( ) ) {
+				for ( const SymbolType & symb : fsm.getInputAlphabet ( ) ) {
+					auto trA = fsm.getTransitions ( ).find ( ext::make_pair ( a, symb ) );
+					auto trB = fsm.getTransitions ( ).find ( ext::make_pair ( b, symb ) );
+
+					if ( trA == fsm.getTransitions ( ).end ( ) && trB == fsm.getTransitions ( ).end ( ) ) {
+						// end up in the same target state (dead state) -> not distinguishable
+					} else if ( trA == fsm.getTransitions ( ).end ( ) || trB == fsm.getTransitions ( ).end ( ) || distinguishable.count ( ext::make_pair ( trA -> second, trB -> second ) ) ) {
+						// end up in dead state  - dead state is be distinguishable from every other state OR
+						// end up in distinguishable states
+						if ( ! distinguishable.count ( ext::make_pair ( a, b ) ) ) { // we have not yet found this
+							distinguishable.insert ( ext::make_pair ( a, b ) );
+							distinguishable.insert ( ext::make_pair ( b, a ) );
+							changed = true;
+						}
+					}
+				}
+			}
+		}
+
+	} while ( changed );
+
+	return distinguishable;
+}
+
+} /* namespace properties */
+
+} /* namespace automaton */
+
+#endif /* DISTINGUISHABLE_STATES_H_ */
diff --git a/alib2algo/test-src/automaton/properties/DistinguishableStatesTest.cpp b/alib2algo/test-src/automaton/properties/DistinguishableStatesTest.cpp
new file mode 100644
index 0000000000..9d241c5e43
--- /dev/null
+++ b/alib2algo/test-src/automaton/properties/DistinguishableStatesTest.cpp
@@ -0,0 +1,97 @@
+#include <catch2/catch.hpp>
+
+#include <automaton/FSM/DFA.h>
+
+#include "automaton/properties/DistinguishableStates.h"
+
+TEST_CASE ( "Distringuishable States Test", "[unit][algo][automaton]" ) {
+	SECTION ( "Test" ) {
+		{
+			DefaultStateType qA ( "qA" );
+			DefaultStateType qB ( "qB" );
+			DefaultStateType qC ( "qC" );
+			DefaultStateType qD ( "qD" );
+			DefaultStateType qE ( "qE" );
+			DefaultStateType qF ( "qF" );
+			DefaultStateType qG ( "qG" );
+			DefaultStateType qH ( "qH" );
+
+			automaton::DFA < > automaton ( qA );
+			automaton.setStates ( { qA, qB, qC, qD, qE, qF, qG, qH } );
+			automaton.setFinalStates ( { qC } );
+			automaton.addInputSymbols ( { DefaultSymbolType ( 0 ), DefaultSymbolType ( 1 ) } );
+
+			automaton.addTransition(qA, DefaultSymbolType ( 0 ), qB);
+			automaton.addTransition(qA, DefaultSymbolType ( 1 ), qF);
+			automaton.addTransition(qB, DefaultSymbolType ( 0 ), qG);
+			automaton.addTransition(qB, DefaultSymbolType ( 1 ), qC);
+			automaton.addTransition(qC, DefaultSymbolType ( 0 ), qA);
+			automaton.addTransition(qC, DefaultSymbolType ( 1 ), qC);
+			automaton.addTransition(qD, DefaultSymbolType ( 0 ), qC);
+			automaton.addTransition(qD, DefaultSymbolType ( 1 ), qG);
+			automaton.addTransition(qE, DefaultSymbolType ( 0 ), qH);
+			automaton.addTransition(qE, DefaultSymbolType ( 1 ), qF);
+			automaton.addTransition(qF, DefaultSymbolType ( 0 ), qC);
+			automaton.addTransition(qF, DefaultSymbolType ( 1 ), qG);
+			automaton.addTransition(qG, DefaultSymbolType ( 0 ), qG);
+			automaton.addTransition(qG, DefaultSymbolType ( 1 ), qE);
+			automaton.addTransition(qH, DefaultSymbolType ( 0 ), qG);
+			automaton.addTransition(qH, DefaultSymbolType ( 1 ), qC);
+
+			ext::set < ext::pair < DefaultStateType, DefaultStateType > > exp;
+			const ext::set < ext::pair < DefaultStateType, DefaultStateType > > res = automaton::properties::DistinguishableStates::distinguishableStates ( automaton );
+			const ext::set < ext::pair < DefaultStateType, DefaultStateType > > exp_ ( {
+					ext::make_pair ( qA, qB ), ext::make_pair ( qA, qC ), ext::make_pair ( qA, qD ), ext::make_pair ( qA, qF ), ext::make_pair ( qA, qG ), ext::make_pair ( qA, qH ),
+					ext::make_pair ( qB, qC ), ext::make_pair ( qB, qD ), ext::make_pair ( qB, qE ), ext::make_pair ( qB, qF ), ext::make_pair ( qB, qG ),
+					ext::make_pair ( qC, qD ), ext::make_pair ( qC, qE ), ext::make_pair ( qC, qF ), ext::make_pair ( qC, qG ), ext::make_pair ( qC, qH ),
+					ext::make_pair ( qD, qE ), ext::make_pair ( qD, qG ), ext::make_pair ( qD, qH ),
+					ext::make_pair ( qE, qF ), ext::make_pair ( qE, qG ), ext::make_pair ( qE, qH ),
+					ext::make_pair ( qF, qG ), ext::make_pair ( qF, qH ),
+					ext::make_pair ( qG, qH ),
+					} );
+
+			for ( const auto & x : exp_ ) {
+				exp.insert ( ext::make_pair ( x.first, x.second ) );
+				exp.insert ( ext::make_pair ( x.second, x.first ) );
+			}
+
+			CHECK ( res == exp );
+		}
+		{
+			DefaultStateType qA ( "qA" );
+			DefaultStateType qB ( "qB" );
+			DefaultStateType qC ( "qC" );
+			DefaultStateType qD ( "qD" );
+			DefaultStateType qE ( "qE" );
+			DefaultStateType qF ( "qF" );
+
+			automaton::DFA < > automaton ( qA );
+			automaton.setStates ( { qA, qB, qC, qD, qE, qF } );
+			automaton.setFinalStates ( { qC, qF } );
+			automaton.addInputSymbols ( { DefaultSymbolType ( 0 ), DefaultSymbolType ( 1 ) } );
+
+			automaton.addTransition(qA, DefaultSymbolType ( 0 ), qB);
+			automaton.addTransition(qA, DefaultSymbolType ( 1 ), qD);
+			automaton.addTransition(qB, DefaultSymbolType ( 0 ), qC);
+			automaton.addTransition(qD, DefaultSymbolType ( 0 ), qE);
+			automaton.addTransition(qE, DefaultSymbolType ( 0 ), qF);
+
+			ext::set < ext::pair < DefaultStateType, DefaultStateType > > exp;
+			const ext::set < ext::pair < DefaultStateType, DefaultStateType > > res = automaton::properties::DistinguishableStates::distinguishableStates ( automaton );
+			const ext::set < ext::pair < DefaultStateType, DefaultStateType > > exp_ ( {
+					ext::make_pair ( qA, qB ), ext::make_pair ( qA, qC ), ext::make_pair ( qA, qD ), ext::make_pair ( qA, qE ), ext::make_pair ( qA, qF ),
+					ext::make_pair ( qB, qC ), ext::make_pair ( qB, qD ), ext::make_pair ( qB, qF ),
+					ext::make_pair ( qC, qD ), ext::make_pair ( qC, qE ),
+					ext::make_pair ( qD, qE ), ext::make_pair ( qD, qF ),
+					ext::make_pair ( qE, qF )
+					} );
+
+			for ( const auto & x : exp_ ) {
+				exp.insert ( ext::make_pair ( x.first, x.second ) );
+				exp.insert ( ext::make_pair ( x.second, x.first ) );
+			}
+
+			CHECK ( res == exp );
+		}
+	}
+}
-- 
GitLab