Skip to content
Snippets Groups Projects
Commit ebc6b852 authored by Jan Travnicek's avatar Jan Travnicek Committed by Jan Trávníček
Browse files

redesign undistinguishable states computation

parent 302a4980
No related branches found
No related tags found
1 merge request!114Merge jt
...@@ -10,16 +10,16 @@ ...@@ -10,16 +10,16 @@
   
namespace { namespace {
   
auto UndistinguishableStatesDFA = registration::AbstractRegister < automaton::properties::UndistinguishableStates, ext::set < ext::set < DefaultStateType > >, const automaton::DFA < > & > ( automaton::properties::UndistinguishableStates::undistinguishable, "fsm" ).setDocumentation ( auto UndistinguishableStatesDFA = registration::AbstractRegister < automaton::properties::UndistinguishableStates, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFA < > & > ( automaton::properties::UndistinguishableStates::undistinguishable, "fsm" ).setDocumentation (
"Computes the partitions of undistinguishable states states in given DFA.\n\ "Computes the partitions of undistinguishable states states in given DFA.\n\
\n\ \n\
@param dfa finite automaton.\n\ @param dfa finite automaton.\n\
@return set of blocks of undistinguishable states" ); @return undistinguishable states relation" );
   
auto UndistinguishableStatesDFTA = registration::AbstractRegister < automaton::properties::UndistinguishableStates, ext::set < ext::set < DefaultStateType > >, const automaton::DFTA < > & > ( automaton::properties::UndistinguishableStates::undistinguishable, "fta" ).setDocumentation ( auto UndistinguishableStatesDFTA = registration::AbstractRegister < automaton::properties::UndistinguishableStates, ext::set < ext::pair < DefaultStateType, DefaultStateType > >, const automaton::DFTA < > & > ( automaton::properties::UndistinguishableStates::undistinguishable, "fta" ).setDocumentation (
"Computes the partitions of undistinguishable states states in given DFTA.\n\ "Computes the partitions of undistinguishable states states in given DFTA.\n\
\n\ \n\
@param dfta finite tree automaton.\n\ @param dfta finite tree automaton.\n\
@return set of blocks of undistinguishable states" ); @return undistinguishable states relation" );
   
} /* namespace */ } /* namespace */
...@@ -42,21 +42,6 @@ namespace properties { ...@@ -42,21 +42,6 @@ namespace properties {
* @sa DistinguishableStates * @sa DistinguishableStates
*/ */
class UndistinguishableStates { class UndistinguishableStates {
template < class StateType >
static ext::set < ext::set < StateType > > convertUndistinguishable ( const ext::set < ext::pair < StateType, StateType > > & undistinguishable, const ext::set < StateType > & states ) {
ext::set < ext::set < StateType > > res;
for ( const StateType & state : states ) {
ext::set < StateType > partition;
for ( const StateType & other : states )
if ( undistinguishable.count ( ext::make_pair ( state, other ) ) != 0 )
partition.insert ( other );
res.insert ( partition );
}
return res;
}
template < class StateType > template < class StateType >
static ext::set < ext::pair < StateType, StateType > > initial ( const ext::set < StateType > & states, const ext::set < StateType > & finals ) { 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; ext::set < ext::pair < StateType, StateType > > init;
...@@ -84,7 +69,7 @@ public: ...@@ -84,7 +69,7 @@ public:
* @return state partitioning of undistinguishable states * @return state partitioning of undistinguishable states
*/ */
template < class SymbolType, class StateType > template < class SymbolType, class StateType >
static ext::set < ext::set < StateType > > undistinguishable ( const automaton::DFA < SymbolType, StateType > & dfa ); static ext::set < ext::pair < StateType, StateType > > undistinguishable ( const automaton::DFA < SymbolType, StateType > & dfa );
   
/** /**
* Creates state partitioning of undistinguishable states- * Creates state partitioning of undistinguishable states-
...@@ -97,11 +82,11 @@ public: ...@@ -97,11 +82,11 @@ public:
* @return state partitioning of undistinguishable states * @return state partitioning of undistinguishable states
*/ */
template < class SymbolType, class StateType > template < class SymbolType, class StateType >
static ext::set < ext::set < StateType > > undistinguishable ( const automaton::DFTA < SymbolType, StateType > & fta ); static ext::set < ext::pair < StateType, StateType > > undistinguishable ( const automaton::DFTA < SymbolType, StateType > & fta );
}; };
   
template < class SymbolType, class StateType > template < class SymbolType, class StateType >
ext::set < ext::set < StateType > > UndistinguishableStates::undistinguishable ( const automaton::DFA < SymbolType, StateType > & dfa ) { ext::set < ext::pair < StateType, StateType > > UndistinguishableStates::undistinguishable ( const automaton::DFA < SymbolType, StateType > & dfa ) {
ext::set < ext::pair < StateType, StateType > > undistinguishable = initial ( dfa.getStates ( ), dfa.getFinalStates ( ) ); ext::set < ext::pair < StateType, StateType > > undistinguishable = initial ( dfa.getStates ( ), dfa.getFinalStates ( ) );
   
do { do {
...@@ -127,11 +112,11 @@ ext::set < ext::set < StateType > > UndistinguishableStates::undistinguishable ( ...@@ -127,11 +112,11 @@ ext::set < ext::set < StateType > > UndistinguishableStates::undistinguishable (
   
} while ( true ); } while ( true );
   
return convertUndistinguishable ( undistinguishable, dfa.getStates ( ) ); return undistinguishable;
} }
   
template < class SymbolType, class StateType > template < class SymbolType, class StateType >
ext::set < ext::set < StateType > > UndistinguishableStates::undistinguishable ( const automaton::DFTA < SymbolType, StateType > & fta ) { ext::set < ext::pair < StateType, StateType > > UndistinguishableStates::undistinguishable ( const automaton::DFTA < SymbolType, StateType > & fta ) {
ext::set < ext::pair < StateType, StateType > > undistinguishable = initial ( fta.getStates ( ), fta.getFinalStates ( ) ); ext::set < ext::pair < StateType, StateType > > undistinguishable = initial ( fta.getStates ( ), fta.getFinalStates ( ) );
   
do { do {
...@@ -161,7 +146,7 @@ ext::set < ext::set < StateType > > UndistinguishableStates::undistinguishable ( ...@@ -161,7 +146,7 @@ ext::set < ext::set < StateType > > UndistinguishableStates::undistinguishable (
   
} while ( true ); } while ( true );
   
return convertUndistinguishable ( undistinguishable, fta.getStates ( ) ); return undistinguishable;
} }
   
} /* namespace properties */ } /* namespace properties */
......
...@@ -21,9 +21,10 @@ static const std::string qGenNFA ( ) { ...@@ -21,9 +21,10 @@ static const std::string qGenNFA ( ) {
   
TEST_CASE ( "Minimization FA test", "[integration]" ) { TEST_CASE ( "Minimization FA test", "[integration]" ) {
static const std::string qDet ( "automaton::determinize::Determinize - | automaton::simplify::Trim -" ); static const std::string qDet ( "automaton::determinize::Determinize - | automaton::simplify::Trim -" );
static const std::string qMinimizeHop ( qDet + " | " + "automaton::simplify::Minimize - | automaton::simplify::Normalize -" ); static const std::string qMinimizeHop ( qDet + " | " + "automaton::simplify::Minimize - | automaton::simplify::Normalize -" );
static const std::string qMinimizeBrz ( qDet + " | " + "automaton::simplify::MinimizeBrzozowski - | automaton::simplify::Trim - | automaton::simplify::Normalize -" ); static const std::string qMinimizeBrz ( qDet + " | " + "automaton::simplify::MinimizeBrzozowski - | automaton::simplify::Trim - | automaton::simplify::Normalize -" );
static const std::string qMinimizeDis ( qDet + " | " + "automaton::simplify::MinimizeByPartitioning - <( $gen | " + qDet + " | automaton::properties::UndistinguishableStates - ) | automaton::simplify::Normalize -" ); static const std::string qMinimizeDis ( qDet + " | " + "automaton::simplify::MinimizeByPartitioning - <( $gen | " + qDet + " | automaton::properties::DistinguishableStates - | relation::RelationComplement - <( $gen | " + qDet + " | automaton::States::get - ) | relation::InducedEquivalence - ) | automaton::simplify::Normalize -" );
static const std::string qMinimizeUnd ( qDet + " | " + "automaton::simplify::MinimizeByPartitioning - <( $gen | " + qDet + " | automaton::properties::UndistinguishableStates - | relation::InducedEquivalence - ) | automaton::simplify::Normalize -" );
   
   
SECTION ( "Files tests" ) { SECTION ( "Files tests" ) {
...@@ -41,6 +42,12 @@ TEST_CASE ( "Minimization FA test", "[integration]" ) { ...@@ -41,6 +42,12 @@ TEST_CASE ( "Minimization FA test", "[integration]" ) {
"quit compare::AutomatonCompare <( $gen | " + qMinimizeHop + " )" + " <( $gen | " + qMinimizeDis + ")" "quit compare::AutomatonCompare <( $gen | " + qMinimizeHop + " )" + " <( $gen | " + qMinimizeDis + ")"
}; };
TimeoutAqlTest ( 2s, qs ); TimeoutAqlTest ( 2s, qs );
qs = {
"execute < " + inputFile + " > $gen",
"quit compare::AutomatonCompare <( $gen | " + qMinimizeHop + " )" + " <( $gen | " + qMinimizeUnd + ")"
};
TimeoutAqlTest ( 2s, qs );
} }
} }
   
...@@ -59,6 +66,12 @@ TEST_CASE ( "Minimization FA test", "[integration]" ) { ...@@ -59,6 +66,12 @@ TEST_CASE ( "Minimization FA test", "[integration]" ) {
"quit compare::AutomatonCompare <( $gen | " + qMinimizeHop + " )" + " <( $gen | " + qMinimizeDis + ")" "quit compare::AutomatonCompare <( $gen | " + qMinimizeHop + " )" + " <( $gen | " + qMinimizeDis + ")"
}; };
TimeoutAqlTest ( 2s, qs ); TimeoutAqlTest ( 2s, qs );
qs = {
qGenNFA ( ) + " > $gen",
"quit compare::AutomatonCompare <( $gen | " + qMinimizeHop + " )" + " <( $gen | " + qMinimizeUnd + ")"
};
TimeoutAqlTest ( 2s, qs );
} }
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment