Skip to content

Commit

Permalink
Merge pull request #307 from VeriFIT/moves
Browse files Browse the repository at this point in the history
Refactor Transitions and Moves
  • Loading branch information
Adda0 authored Sep 1, 2023
2 parents 2634c92 + 87271aa commit f5fbdb0
Show file tree
Hide file tree
Showing 16 changed files with 737 additions and 594 deletions.
33 changes: 18 additions & 15 deletions bindings/python/libmata/nfa/nfa.pxd
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,20 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
COrdVector[CSymbolPost].const_iterator cbegin()
COrdVector[CSymbolPost].const_iterator cend()

cdef cppclass CTransitions "mata::nfa::Delta::Transitions":
cppclass const_iterator:
bool operator==(const_iterator&)
bool operator!=(const_iterator&)
CTrans& operator*()
const_iterator& operator++()
const_iterator begin()
const_iterator end()
CTransitions()


cdef cppclass CDelta "mata::nfa::Delta":
vector[CStatePost] post
vector[CStatePost] state_posts
CTransitions transitions

void reserve(size_t)
CStatePost& state_post(State)
Expand All @@ -70,6 +82,8 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
bool contains(State, Symbol, State)
COrdVector[CSymbolPost].const_iterator epsilon_symbol_posts(State state, Symbol epsilon)
COrdVector[CSymbolPost].const_iterator epsilon_symbol_posts(CStatePost& post, Symbol epsilon)
size_t num_of_transitions()
CTransitions transitions()

cdef cppclass CRun "mata::nfa::Run":
# Public Attributes
Expand Down Expand Up @@ -109,16 +123,10 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
bool operator>(CSymbolPost)
bool operator>=(CSymbolPost)

cdef cppclass CNfa "mata::nfa::Nfa":
# Nested iterator
cppclass const_iterator:
const_iterator()
CTrans operator*()
const_iterator& operator++()
bool operator==(const_iterator&)
bool operator!=(const_iterator&)
void refresh_trans()
COrdVector[State].const_iterator begin()
COrdVector[State].const_iterator end()

cdef cppclass CNfa "mata::nfa::Nfa":
# Public Attributes
CSparseSet[State] initial
CSparseSet[State] final
Expand Down Expand Up @@ -146,16 +154,11 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
void unify_final()
COrdVector[Symbol] get_used_symbols()
bool is_state(State)
size_t get_num_of_trans()
StateSet post(StateSet&, Symbol)
CNfa.const_iterator begin()
CNfa.const_iterator end()
State add_state()
State add_state(State)
void print_to_DOT(ostream)
vector[CTrans] get_transitions_to(State)
vector[CTrans] get_trans_as_sequence()
vector[CTrans] get_trans_from_as_sequence(State)
CNfa& trim(StateRenaming*)
void get_one_letter_aut(CNfa&)
bool is_epsilon(Symbol)
Expand Down
31 changes: 22 additions & 9 deletions bindings/python/libmata/nfa/nfa.pyx
Original file line number Diff line number Diff line change
Expand Up @@ -379,12 +379,12 @@ cdef class Nfa:
"""
return self.thisptr.get().delta.contains(source, symbol, target)

def get_num_of_trans(self):
def get_num_of_transitions(self):
"""Returns number of transitions in automaton
:return: number of transitions in automaton
"""
return self.thisptr.get().get_num_of_trans()
return self.thisptr.get().delta.num_of_transitions()

def clear(self):
"""Clears all of the internals in the automaton"""
Expand All @@ -401,8 +401,9 @@ cdef class Nfa:
:return: stream of transitions
"""
iterator = self.thisptr.get().begin()
while iterator != self.thisptr.get().end():
cdef CTransitions transitions = self.thisptr.get().delta.transitions()
cdef CTransitions.const_iterator iterator = transitions.begin()
while iterator != transitions.end():
trans = Transition()
lhs = dereference(iterator)
trans.copy_from(lhs)
Expand Down Expand Up @@ -444,23 +445,35 @@ cdef class Nfa:
def get_trans_as_sequence(self):
"""Get automaton transitions as a sequence.
TODO: Refactor into a generator.
:return: List of automaton transitions.
"""
cdef vector[CTrans] c_transitions = self.thisptr.get().get_trans_as_sequence()
cdef CTransitions c_transitions = self.thisptr.get().delta.transitions()
transitions = []
for c_transition in c_transitions:
transitions.append(Transition(c_transition.source, c_transition.symbol, c_transition.target))
return transitions

def get_trans_from_state_as_sequence(self, State state_from):
def get_trans_from_state_as_sequence(self, State source) -> list[Transition]:
"""Get automaton transitions from state_from as a sequence.

TODO: Refactor into a generator.

:return: List of automaton transitions.
"""
cdef vector[CTrans] c_transitions = self.thisptr.get().get_trans_from_as_sequence(state_from)
transitions = []
for c_transition in c_transitions:
transitions.append(Transition(c_transition.source, c_transition.symbol, c_transition.target))
cdef CStatePost c_state_post = self.thisptr.get().delta[source]
cdef COrdVector[CSymbolPost].const_iterator c_state_post_it = c_state_post.cbegin()
cdef CSymbolPost c_symbol_post
cdef COrdVector[State].const_iterator c_symbol_post_it
while c_state_post_it != c_state_post.cend():
c_symbol_post = dereference(c_state_post_it)
c_symbol_post_it = c_symbol_post.begin()
while c_symbol_post_it != c_symbol_post.end():
transitions.append(Transition(source, c_symbol_post.symbol, dereference(c_symbol_post_it)))
preinc(c_symbol_post_it)
preinc(c_state_post_it)
return transitions

def get_useful_states(self):
Expand Down
22 changes: 11 additions & 11 deletions bindings/python/tests/test_nfa.py
Original file line number Diff line number Diff line change
Expand Up @@ -502,7 +502,7 @@ def test_intersection_preserving_epsilon_transitions():
assert len(result.final_states) == 4

# Check transitions.
assert result.get_num_of_trans() == 15
assert result.get_num_of_transitions() == 15

assert result.has_transition(product_map[(0, 0)], mata_nfa.epsilon(), product_map[(1, 0)])
assert len(result.get_trans_from_state_as_sequence(product_map[(0, 0)])) == 1
Expand Down Expand Up @@ -591,11 +591,11 @@ def test_minimize(
fa_one_divisible_by_two, fa_one_divisible_by_four, fa_one_divisible_by_eight
):
minimized = mata_nfa.minimize(fa_one_divisible_by_two)
assert minimized.get_num_of_trans() <= fa_one_divisible_by_two.get_num_of_trans()
assert minimized.get_num_of_transitions() <= fa_one_divisible_by_two.get_num_of_transitions()
minimized = mata_nfa.minimize(fa_one_divisible_by_four)
assert minimized.get_num_of_trans() <= fa_one_divisible_by_four.get_num_of_trans()
assert minimized.get_num_of_transitions() <= fa_one_divisible_by_four.get_num_of_transitions()
minimized = mata_nfa.minimize(fa_one_divisible_by_eight)
assert minimized.get_num_of_trans() <= fa_one_divisible_by_eight.get_num_of_trans()
assert minimized.get_num_of_transitions() <= fa_one_divisible_by_eight.get_num_of_transitions()

lhs = mata_nfa.Nfa(11)
lhs.make_initial_state(0)
Expand All @@ -604,10 +604,10 @@ def test_minimize(
lhs.make_final_state(i)
lhs.add_transition(10, 0, 10)
lhs.make_final_state(10)
assert lhs.get_num_of_trans() == 11
assert lhs.get_num_of_transitions() == 11

minimized = mata_nfa.minimize(lhs)
assert minimized.get_num_of_trans() == 1
assert minimized.get_num_of_transitions() == 1


def test_to_dot():
Expand Down Expand Up @@ -665,7 +665,7 @@ def test_trim(prepare_automaton_a):

nfa.remove_final_state(2) # '2' is the new final state in the earlier trimmed automaton.
nfa.trim()
assert nfa.get_num_of_trans() == 0
assert nfa.get_num_of_transitions() == 0
assert nfa.size() == 0


Expand All @@ -677,7 +677,7 @@ def test_get_one_letter_automaton(prepare_automaton_a):
one_letter_automaton = nfa.get_one_letter_aut()

assert one_letter_automaton.size() == nfa.size()
assert one_letter_automaton.get_num_of_trans() == 12
assert one_letter_automaton.get_num_of_transitions() == 12
assert one_letter_automaton.has_transition(1, abstract_symbol, 10)
assert one_letter_automaton.has_transition(10, abstract_symbol, 7)
assert not one_letter_automaton.has_transition(10, ord('a'), 7)
Expand Down Expand Up @@ -896,7 +896,7 @@ def test_reduce():

# Test the reduction of an empty automaton.
result, state_map = mata_nfa.reduce_with_state_map(nfa)
assert result.get_num_of_trans() == 0
assert result.get_num_of_transitions() == 0
assert len(result.initial_states) == 0
assert len(result.final_states) == 0

Expand All @@ -905,15 +905,15 @@ def test_reduce():
nfa.make_initial_state(1)
nfa.make_final_state(2)
result, state_map = mata_nfa.reduce_with_state_map(nfa)
assert result.get_num_of_trans() == 0
assert result.get_num_of_transitions() == 0
assert result.size() == 2
assert result.has_initial_state(state_map[1])
assert result.has_final_state(state_map[2])
assert state_map[1] == state_map[0]
assert state_map[2] != state_map[0]

result, state_map = mata_nfa.reduce_with_state_map(nfa.trim())
assert result.get_num_of_trans() == 0
assert result.get_num_of_transitions() == 0
assert result.size() == 0

# Test the reduction of a bigger automaton.
Expand Down
10 changes: 5 additions & 5 deletions bindings/python/tests/test_trans.py
Original file line number Diff line number Diff line change
Expand Up @@ -98,22 +98,22 @@ def test_transitions():
t4 = mata_nfa.Transition(2, 2, 2)

# Test adding transition.
assert lhs.get_num_of_trans() == 0
assert lhs.get_num_of_transitions() == 0
lhs.add_transition(0, 0, 0)
assert lhs.get_num_of_trans() == 1
assert lhs.get_num_of_transitions() == 1
assert lhs.has_transition(t1.source, t1.symbol, t1.target)

lhs.add_transition_object(t2)
assert lhs.get_num_of_trans() == 2
assert lhs.get_num_of_transitions() == 2
assert lhs.has_transition(t2.source, t2.symbol, t2.target)

# Test adding add-hoc transition.
lhs.add_transition(1, 1, 1)
assert lhs.get_num_of_trans() == 3
assert lhs.get_num_of_transitions() == 3
assert lhs.has_transition(t3.source, t3.symbol, t3.target)
assert not lhs.has_transition(2, 2, 2)
lhs.add_transition_object(t4)
assert lhs.get_num_of_trans() == 4
assert lhs.get_num_of_transitions() == 4
assert lhs.has_transition(2, 2, 2)

# Test that transitions are not duplicated.
Expand Down
Loading

0 comments on commit f5fbdb0

Please sign in to comment.