Permalink
Browse files

Generalize DFA equivalence algorithm under TransitionSystem::Equivale…

…nce.
  • Loading branch information...
1 parent e5d7bc6 commit 819e2103c50083d1271ef27baf9d52180ccdb2e6 @blambeau committed Jul 23, 2012
View
@@ -1,7 +1,8 @@
-# 0.5.5 / FIX ME
+# 0.6.0 / FIX ME
* Generalized the decoration algorithm to work backwards as well as forwards as well as
accepting an output Hash-like object, defaulting to true state decorations.
+* Generalized the DFA equivalence algorithm under TransitionSystem::Equivalence.
# O.5.4 / 2012-03-06
@@ -1,54 +1,36 @@
module Stamina
class Automaton
+ # Implements the equivalence relation commonly used on canonical DFAs
+ class Equivalence < TransitionSystem::Equivalence
+
+ def equivalent_systems?(s, t)
+ (s.state_count == t.state_count) &&
+ (s.edge_count == t.edge_count) &&
+ (s.alphabet == t.alphabet) &&
+ (s.data == t.data)
+ end
+
+ def equivalent_states?(s, t)
+ (s.initial? == t.initial?) &&
+ (s.accepting? == t.accepting?) &&
+ (s.error? == t.error?)
+ end
+
+ def equivalent_edges?(e, f)
+ e.symbol == f.symbol
+ end
+
+ end # class Equivalence
+
#
# Checks if this automaton is equivalent to another one.
#
# Automata must be both minimal and complete to guarantee that this method
# works.
#
- def equivalent?(other, equiv = nil, key = :equiv_state)
- equiv ||= Proc.new{|s1,s2| (s1 && s2) &&
- (s1.accepting? == s2.accepting?) &&
- (s1.error? == s2.error?) &&
- (s1.initial? == s2.initial?) }
-
- # Both must already have basic attributes in common
- return false unless state_count==other.state_count
- return false unless edge_count==other.edge_count
- return false unless alphabet==other.alphabet
- return false unless equiv[initial_state, other.initial_state]
-
- # We instantiate the decoration algorithm for checking equivalence on this
- # automaton:
- # * decoration is the index of the equivalent state in other automaton
- # * d0 is thus 'other.initial_state.index'
- # * suppremum is identity and fails when the equivalent state is not unique
- # * propagation checks transition function delta
- #
- algo = Stamina::Utils::Decorate.new
- algo.set_suppremum do |d0, d1|
- if (d0.nil? or d1.nil?)
- (d0 || d1)
- else
- throw :non_equivalent unless d0==d1
- d0
- end
- end
- algo.set_initiator{|s| s.initial? ? other.initial_state.index : nil}
- algo.set_start_predicate{|s| s.initial? }
- algo.set_propagate do |d,e|
- reached = other.ith_state(d).dfa_step(e.symbol)
- throw :non_equivalent unless reached && equiv[e.target, reached]
- reached.index
- end
-
- # Run the algorithm now
- catch(:non_equivalent) do
- algo.call(self, key)
- return true
- end
- return false
+ def equivalent?(other)
+ Equivalence.new.call(self, other)
end
alias :<=> :equivalent?
@@ -2,9 +2,10 @@
require_relative 'errors'
require_relative 'ext/math'
require_relative 'markable'
+require_relative 'utils'
+require_relative 'transition_system'
require_relative 'adl'
require_relative 'automaton'
-require_relative 'utils'
require_relative 'input_string'
require_relative 'sample'
require_relative 'dsl'
@@ -0,0 +1 @@
+require_relative 'transition_system/equivalence'
@@ -0,0 +1,69 @@
+module Stamina
+ class TransitionSystem
+ class Equivalence
+
+ # Returns true if `s` and `t` must be considered equivalent, false otherwise.
+ def equivalent_systems?(s, t)
+ (s.state_count == t.state_count) &&
+ (s.edge_count == t.edge_count) &&
+ (s.data == t.data)
+ end
+
+ # Returns true if `s` and `t` must be considered equivalent, false otherwise.
+ def equivalent_states?(s, t)
+ s.data == t.data
+ end
+
+ # Returns true if `e` and `f` must be considered equivalent, false otherwise.
+ def equivalent_edges?(e, f)
+ e.data == f.data
+ end
+
+ # Computes equivalence pairs through decoration
+ class EquivThroughDeco < Utils::Decorate
+
+ def initialize(algo, reference)
+ @algo = algo
+ @reference = reference
+ end
+ attr_reader :reference, :algo
+
+ def suppremum(d0, d1)
+ return (d0 || d1) if (d0.nil? or d1.nil?)
+ throw :not_equivalent unless d0==d1
+ d0
+ end
+
+ def propagate(deco, edge)
+ symbol = edge.symbol
+ eq_edge = reference.ith_state(deco).out_edges.find{|e| e.symbol==symbol}
+ throw :non_equivalent unless eq_edge && algo.equivalent_edges?(edge, eq_edge)
+ throw :non_equivalent unless algo.equivalent_states?(edge.target, eq_edge.target)
+ eq_edge.target.index
+ end
+
+ def init_deco(s)
+ s.initial? ? reference.initial_state.index : nil
+ end
+
+ def take_at_start?(s)
+ s.initial?
+ end
+
+ end # EquivThroughDeco
+
+ # Executes the equivalence algorithm on two transition systems `ts1` and `ts2`.
+ # Returns true if they are considered equivalent, false otherwise.
+ def call(ts1, ts2)
+ return false unless equivalent_systems?(ts1, ts2)
+ return false unless equivalent_states?(ts1.initial_state, ts2.initial_state)
+ catch(:non_equivalent) do
+ EquivThroughDeco.new(self, ts2).call(ts1, {})
+ return true
+ end
+ return false
+ end
+
+ end # class Equivalence
+ end # class TransitionSystem
+end # module Stamina

0 comments on commit 819e210

Please sign in to comment.