From c75612e989e13781119e780ad780e673139ec30d Mon Sep 17 00:00:00 2001
From: Tomas Pecka <tomas.pecka@fit.cvut.cz>
Date: Sun, 8 Mar 2020 12:00:51 +0100
Subject: [PATCH] algo: Add algorithm for existence of a synchronizing word on
DFA
---
.../properties/SynchronizingWordExistence.cpp | 19 ++++
.../properties/SynchronizingWordExistence.h | 96 +++++++++++++++++++
.../properties/SynchronizingWordExistence.cpp | 58 +++++++++++
3 files changed, 173 insertions(+)
create mode 100644 alib2algo/src/automaton/properties/SynchronizingWordExistence.cpp
create mode 100644 alib2algo/src/automaton/properties/SynchronizingWordExistence.h
create mode 100644 alib2algo/test-src/automaton/properties/SynchronizingWordExistence.cpp
diff --git a/alib2algo/src/automaton/properties/SynchronizingWordExistence.cpp b/alib2algo/src/automaton/properties/SynchronizingWordExistence.cpp
new file mode 100644
index 0000000000..7adb81dbfb
--- /dev/null
+++ b/alib2algo/src/automaton/properties/SynchronizingWordExistence.cpp
@@ -0,0 +1,19 @@
+/*
+ * SynchronizingWordExistence.cpp
+ *
+ * Created on: 8. 3. 2020
+ * Author: Tomas Pecka
+ */
+
+#include "SynchronizingWordExistence.h"
+#include <registration/AlgoRegistration.hpp>
+
+namespace {
+
+auto SynchronizingWordExistenceDFA = registration::AbstractRegister < automaton::properties::SynchronizingWordExistence, bool, const automaton::DFA < > & > ( automaton::properties::SynchronizingWordExistence::exists, "dfa" ).setDocumentation (
+"Checks whether the given DFA has a synchronizing word.\n\
+\n\
+@param dfa automaton\n\
+@return boolean indicating whether the automaton has a synchronizing word" );
+
+} /* namespace */
diff --git a/alib2algo/src/automaton/properties/SynchronizingWordExistence.h b/alib2algo/src/automaton/properties/SynchronizingWordExistence.h
new file mode 100644
index 0000000000..1cf13953a9
--- /dev/null
+++ b/alib2algo/src/automaton/properties/SynchronizingWordExistence.h
@@ -0,0 +1,96 @@
+/*
+ * SynchronizingWordExistence.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: 8. 3. 2020
+ * Author: Tomas Pecka
+ */
+
+#ifndef SYNCHRONIZING_WORD_EXISTENCE_H_
+#define SYNCHRONIZING_WORD_EXISTENCE_H_
+
+#include <alib/set>
+#include <queue>
+
+#include <automaton/FSM/DFA.h>
+#include <automaton/transform/AutomataIntersectionCartesianProduct.h>
+
+namespace automaton::properties {
+
+/**
+ * Algorithm determining the existence of a synchronizing word on an automaton.
+ */
+class SynchronizingWordExistence {
+public:
+ /**
+ * Checks whether the given DFA has a synchronizing word.
+ *
+ * @param dfa automaton
+ * @return boolean indicating whether the automaton has a synchronizing word
+ */
+ template < class SymbolType, class StateType >
+ static bool exists ( const automaton::DFA < SymbolType, StateType > & dfa );
+};
+
+template < class SymbolType, class StateType >
+bool SynchronizingWordExistence::exists ( const automaton::DFA < SymbolType, StateType > & dfa ) {
+ /*
+ * It must hold that (1) <=> (2)
+ * (1) DFA is synchronizing
+ * (2) Foreach q1, q2 in Q, exists a word w such that \delta(q1, w) = \delta(q2, w)
+ */
+
+ /* Therefore the algorithm is as follows:
+ * Create a parallel run of the automaton with itseld
+ * All pairs (q1, q2) \in Q x Q MUST have a path to some state-pair (q, q).
+ * -> For every pair (q,q) run a BFS search and check that all pairs (q1, q2) are visited
+ */
+
+ automaton::DFA < SymbolType, ext::pair < StateType, StateType > > cart = automaton::transform::AutomataIntersectionCartesianProduct:: intersection ( dfa, dfa );
+
+ std::queue < ext::pair < StateType, StateType > > q;
+ ext::set < ext::pair < StateType, StateType > > visited;
+
+ for ( const ext::pair < StateType, StateType > state: cart.getStates ( ) ) {
+ if ( state.first != state.second )
+ continue;
+
+ visited.insert ( state );
+ q.push ( state );
+ }
+
+ while ( ! q.empty ( ) ) {
+ const ext::pair < StateType, StateType > cstate = std::move ( q.front ( ) );
+ q.pop ( );
+
+ for ( const auto transition : cart.getTransitionsToState ( cstate ) ) {
+ const auto & srcState = transition.first.first;
+
+ if ( visited.count ( srcState ) == 0 ) {
+ visited.insert ( srcState );
+ q.push ( srcState );
+ }
+ }
+ }
+
+ return visited == cart.getStates ( );
+}
+
+} /* namespace automaton::properties */
+
+#endif /* SYNCHRONIZING_WORD_EXISTENCE_H_ */
diff --git a/alib2algo/test-src/automaton/properties/SynchronizingWordExistence.cpp b/alib2algo/test-src/automaton/properties/SynchronizingWordExistence.cpp
new file mode 100644
index 0000000000..c43d722c37
--- /dev/null
+++ b/alib2algo/test-src/automaton/properties/SynchronizingWordExistence.cpp
@@ -0,0 +1,58 @@
+#include <catch2/catch.hpp>
+
+#include <automaton/FSM/DFA.h>
+
+#include "automaton/properties/SynchronizingWordExistence.h"
+
+TEST_CASE ( "Synchronizing Word Existence", "[unit][algo][automaton]" ) {
+ SECTION ( "Test 1" ) {
+ DefaultStateType q1 = DefaultStateType ("q1");
+ DefaultStateType q2 = DefaultStateType ("q2");
+ DefaultStateType q3 = DefaultStateType ("q3");
+
+ DefaultSymbolType a = DefaultSymbolType ("a");
+ DefaultSymbolType b = DefaultSymbolType ("b");
+
+ automaton::DFA< > automaton(q1);
+ automaton.addInputSymbols({a, b});
+ automaton.setStates({q1, q2, q3});
+
+ automaton.addTransition(q1, a, q1);
+ automaton.addTransition(q2, a, q2);
+ automaton.addTransition(q3, a, q3);
+ automaton.addTransition(q1, b, q2);
+ automaton.addTransition(q2, b, q3);
+ automaton.addTransition(q3, b, q1);
+
+ CHECK(! automaton::properties::SynchronizingWordExistence::exists(automaton));
+ }
+
+ SECTION ( "Test 2" ) {
+ DefaultStateType q0 = DefaultStateType ("q0");
+ DefaultStateType q1 = DefaultStateType ("q1");
+ DefaultStateType q2 = DefaultStateType ("q2");
+ DefaultStateType q3 = DefaultStateType ("q3");
+ DefaultStateType q4 = DefaultStateType ("q4");
+
+ DefaultSymbolType a = DefaultSymbolType ("a");
+ DefaultSymbolType b = DefaultSymbolType ("b");
+
+ automaton::DFA< > automaton(q0);
+ automaton.addInputSymbols({a, b});
+ automaton.setStates({q0, q1, q2, q3, q4});
+
+ automaton.addTransition(q0, a, q1);
+ automaton.addTransition(q1, a, q1);
+ automaton.addTransition(q2, a, q2);
+ automaton.addTransition(q3, a, q3);
+ automaton.addTransition(q4, a, q4);
+
+ automaton.addTransition(q0, b, q1);
+ automaton.addTransition(q1, b, q2);
+ automaton.addTransition(q2, b, q3);
+ automaton.addTransition(q3, b, q4);
+ automaton.addTransition(q4, b, q0);
+
+ CHECK(automaton::properties::SynchronizingWordExistence::exists(automaton));
+ }
+}
--
GitLab