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

fix bisimulation implementation

parent 507011d1
No related branches found
No related tags found
1 merge request!120Merge jt
...@@ -118,14 +118,14 @@ ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBi ...@@ -118,14 +118,14 @@ ext::set < ext::pair < StateType, StateType > > BackwardBisimulation::backwardBi
if ( ! backwardBisimulation.contains ( ext::make_pair ( p, q ) ) ) if ( ! backwardBisimulation.contains ( ext::make_pair ( p, q ) ) )
continue; continue;
   
for ( const std::pair < const ext::pair < SymbolType, StateType >, StateType > & pTransition : fta.getTransitionsToState ( p ) ) { for ( const std::pair < const ext::pair < StateType, SymbolType >, StateType > & pTransition : fta.getTransitionsToState ( p ) ) {
   
bool exists = false; bool exists = false;
for ( const std::pair < const ext::pair < SymbolType, StateType >, StateType > & qTransition : fta.getTransitionsToState ( q ) ) { for ( const std::pair < const ext::pair < StateType, SymbolType >, StateType > & qTransition : fta.getTransitionsToState ( q ) ) {
if ( qTransition.first.first != pTransition.first.first ) if ( qTransition.first.second != pTransition.first.second )
continue; continue;
   
if ( backwardBisimulation.contains ( ext::make_pair ( pTransition.first.second, qTransition.first.second) ) ) { if ( backwardBisimulation.contains ( ext::make_pair ( pTransition.first.first, qTransition.first.first ) ) ) {
exists = true; exists = true;
break; break;
} }
......
...@@ -119,11 +119,17 @@ ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisi ...@@ -119,11 +119,17 @@ ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisi
if ( ! forwardBisimulation.contains ( ext::make_pair ( p, q ) ) ) if ( ! forwardBisimulation.contains ( ext::make_pair ( p, q ) ) )
continue; continue;
   
for ( const std::pair < const ext::pair < SymbolType, StateType >, StateType > & transition : fta.getTransitions ( ) ) { for ( const std::pair < const ext::pair < StateType, SymbolType >, StateType > & pTransition : fta.getTransitions ( ) ) {
if ( transition.first.second == p ) { if ( pTransition.first.first == p ) {
const auto & transition2 = fta.getTransitions ( ).find ( std::make_pair ( transition.first.first, q ) ); bool exists = false;
for ( const std::pair < const ext::pair < StateType, SymbolType >, StateType > & qTransition : fta.getTransitions ( ).equal_range ( std::make_pair ( q, pTransition.first.second ) ) ) {
if ( forwardBisimulation.contains ( ext::make_pair ( pTransition.second, qTransition.second ) ) ) {
exists = true;
break;
}
}
   
if ( transition2 == fta.getTransitions ( ).end ( ) || ! forwardBisimulation.contains ( ext::make_pair ( transition.second, transition2->second ) ) ) { if ( ! exists ) {
forwardBisimulation.erase ( ext::make_pair ( p, q ) ); forwardBisimulation.erase ( ext::make_pair ( p, q ) );
forwardBisimulation.erase ( ext::make_pair ( q, p ) ); forwardBisimulation.erase ( ext::make_pair ( q, p ) );
changed = true; changed = true;
...@@ -155,15 +161,21 @@ ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisi ...@@ -155,15 +161,21 @@ ext::set < ext::pair < StateType, StateType > > ForwardBisimulation::forwardBisi
if ( ! forwardBisimulation.contains ( ext::make_pair ( p, q ) ) ) if ( ! forwardBisimulation.contains ( ext::make_pair ( p, q ) ) )
continue; continue;
   
for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::vector < StateType > >, StateType > & transition : fta.getTransitions ( ) ) { for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::vector < StateType > >, StateType > & pTransition : fta.getTransitions ( ) ) {
for ( size_t i = 0; i < transition.first.second.size ( ); ++ i ) { for ( size_t i = 0; i < pTransition.first.second.size ( ); ++ i ) {
if ( transition.first.second [ i ] == p ) { if ( pTransition.first.second [ i ] == p ) {
ext::vector < StateType > copy = transition.first.second; ext::vector < StateType > copy = pTransition.first.second;
copy [ i ] = q; copy [ i ] = q;
   
const auto & transition2 = fta.getTransitions ( ).find ( std::make_pair ( transition.first.first, std::move ( copy ) ) ); bool exists = false;
for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType >, ext::vector < 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 ( transition2 == fta.getTransitions ( ).end ( ) || ! forwardBisimulation.contains ( ext::make_pair ( transition.second, transition2->second ) ) ) { if ( ! exists ) {
forwardBisimulation.erase ( ext::make_pair ( p, q ) ); forwardBisimulation.erase ( ext::make_pair ( p, q ) );
forwardBisimulation.erase ( ext::make_pair ( q, p ) ); forwardBisimulation.erase ( ext::make_pair ( q, p ) );
changed = true; changed = true;
......
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