From 1f26c0e9ddfebba82d4ddb34262993d1c5c5b9bb Mon Sep 17 00:00:00 2001
From: Cristian-Ioan Vasile <cvasile@mit.edu>
Date: Wed, 22 Mar 2023 22:54:19 -0400
Subject: [PATCH 1/9] Updated model module.

---
 lomap/classes/model.py | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/lomap/classes/model.py b/lomap/classes/model.py
index db95f93..11a19f4 100644
--- a/lomap/classes/model.py
+++ b/lomap/classes/model.py
@@ -68,7 +68,7 @@ def __eq__(self, other):
             and self.directed == other.directed and self.multi == other.multi
             and self.init == other.init and self.final == other.final
             #FIXME: Incompatible with nx2.0
-            and self.g.node == other.g.node and self.g.edge == other.g.edge)
+            and nx.graphs_equal(self.g, other.g)
 
     def __ne__(self, other):
         '''Equality testing. See `Model.__eq__()`.'''
@@ -78,11 +78,9 @@ def nodes_w_prop(self, propset):
         """
         Returns the set of nodes with given properties.
         """
-        nodes_w_prop = set()
-        for node, data in self.g.nodes(data=True):
-            if propset <= data.get('prop',set()):
-                nodes_w_prop.add(node)
-        return nodes_w_prop
+        return set(node
+                    for node, props in self.g.nodes(data='prop', default=set())
+                        if propset <= props))
 
     def size(self):
         return (self.g.number_of_nodes(), self.g.number_of_edges())
@@ -92,6 +90,7 @@ def visualize(self, edgelabel=None, draw='pygraphviz'):
         Visualizes a LOMAP system model
         """
         if draw == 'pygraphviz':
+            raise NotImplementedError
             nx.view_pygraphviz(self.g, edgelabel)
         elif draw == 'matplotlib':
             pos = nx.spring_layout(self.g)
@@ -99,7 +98,7 @@ def visualize(self, edgelabel=None, draw='pygraphviz'):
             nx.draw_networkx_labels(self.g, pos=pos)
         else:
             raise ValueError('Expected parameter draw to be either:'
-                             + '"pygraphviz" or "matplotlib"!')
+                             '"matplotlib"!')
 
     @classmethod
     def load(cls, filename):

From 8132d13bfc738b34b135024cecfe6b3e3dc05d8e Mon Sep 17 00:00:00 2001
From: Cristian-Ioan Vasile <cvasile@mit.edu>
Date: Wed, 22 Mar 2023 22:54:54 -0400
Subject: [PATCH 2/9] Started to update automata.

---
 lomap/classes/automata.py | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/lomap/classes/automata.py b/lomap/classes/automata.py
index f724fa4..3ada933 100644
--- a/lomap/classes/automata.py
+++ b/lomap/classes/automata.py
@@ -166,8 +166,8 @@ def next_states(self, q, props):
         # Get the bitmap representation of props
         prop_bitmap = self.bitmap_of_props(props)
         # Return an array of next states
-        return [v for _, v, d in self.g.out_edges_iter(q, data=True)
-                                                   if prop_bitmap in d['input']]
+        return [v for _, v, input in self.g.out_edges(q, data='input')
+                                                        if prop_bitmap in input]
 
     def next_state(self, q, props):
         """
@@ -179,8 +179,8 @@ def next_state(self, q, props):
         # Get the bitmap representation of props
         prop_bitmap = self.bitmap_of_props(props)
         # Return an array of next states
-        nq = [v for _, v, d in self.g.out_edges_iter(q, data=True)
-                                                   if prop_bitmap in d['input']]
+        nq = [v for _, v, input in self.g.out_edges(q, data='input')
+                                                        if prop_bitmap in input]
         assert len(nq) <= 1
         if nq:
             return nq[0]
@@ -240,9 +240,8 @@ def add_trap_state(self):
         """
         trap_added = False
         for s in self.g:
-            rem_alphabet = set(self.alphabet)
-            for _, _, d in self.g.out_edges_iter(s, data=True):
-                rem_alphabet -= d['input']
+            rem_alphabet = set(self.alphabet) \
+                - set(input for _, _, input in self.g.out_edges(s, data='input')
             if rem_alphabet:
                 if not trap_added: #'trap' not in self.g:
                     self.g.add_node('trap')

From ce1e85af95b5e5b59258e6eeb4e0ccb661513a2f Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:10:10 -0400
Subject: [PATCH 3/9] Updated model and automata.

---
 lomap/classes/__init__.py |  15 ++-
 lomap/classes/automata.py | 221 +++++++++++++++++---------------------
 lomap/classes/model.py    |  21 ++--
 3 files changed, 118 insertions(+), 139 deletions(-)

diff --git a/lomap/classes/__init__.py b/lomap/classes/__init__.py
index 0739157..b0edadb 100644
--- a/lomap/classes/__init__.py
+++ b/lomap/classes/__init__.py
@@ -1,8 +1,7 @@
 #! /usr/bin/python
 
-from __future__ import absolute_import
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
-#               2015-2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+#               2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -24,7 +23,7 @@
 from lomap.classes.ts import Ts
 from lomap.classes.markov import Markov
 from lomap.classes.timer import Timer
-from lomap.classes.interval import Interval
+
 
 def model_representer(dumper, model,
                       init_representer=list, final_representer=list):
@@ -51,7 +50,7 @@ def model_constructor(loader, node, ModelClass,
     data = loader.construct_mapping(node, deep=True)
     name = data.get('name', 'Unnamed')
     directed = data.get('directed', True)
-    multi = data.get('multi', True)
+    multi = data.get('multi', False)
 
     model = ModelClass(name=name, directed=directed, multi=multi)
     model.init = init_factory(data.get('init', init_factory()))
@@ -68,7 +67,7 @@ def automaton_representer(dumper, automaton):
         'name'     : automaton.name,
         'props'    : automaton.props,
         'multi'    : automaton.multi,
-        'init'     : automaton.init, #FIXME: Why is init a dict?
+        'init'     : automaton.init,
         'final'    : automaton.final, #FIXME: list causes errors with Rabin
         'graph'    : {
             'nodes' : dict(automaton.g.nodes(data=True)),
@@ -76,15 +75,15 @@ def automaton_representer(dumper, automaton):
             }
         })
 
-def automaton_constructor(loader, node, ModelClass, # FIXME: Why is init a dict?
-                      init_factory=dict, final_factory=set):
+def automaton_constructor(loader, node, ModelClass,
+                          init_factory=set, final_factory=set):
     '''Model constructor from YAML document.
     Note: Creates an object of class ModelClass.
     '''
     data = loader.construct_mapping(node, deep=True)
     name = data.get('name', 'Unnamed')
     props = data.get('props', None)
-    multi = data.get('multi', True)
+    multi = data.get('multi', False)
 
     automaton = ModelClass(name=name, props=props, multi=multi)
     automaton.init = init_factory(data.get('init', init_factory()))
diff --git a/lomap/classes/automata.py b/lomap/classes/automata.py
index 3ada933..7e9ed49 100644
--- a/lomap/classes/automata.py
+++ b/lomap/classes/automata.py
@@ -1,7 +1,7 @@
 #! /usr/bin/python
 
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
-#               2015-2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+#               2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -32,7 +32,7 @@
 
 # Logger configuration
 logger = logging.getLogger(__name__)
-#logger.addHandler(logging.NullHandler())
+
 
 '''
 These variables define to which encoding the outputs of these programs
@@ -50,17 +50,17 @@
 
 
 class Automaton(Model):
-    """
+    '''
     Base class for deterministic or non-deterministic automata.
-    """
+    '''
 
     yaml_tag = u'!Automaton'
 
-    def __init__(self, name= 'Unnamed automaton', props=None, multi=True):
-        """
-        LOMAP Automaton object constructor
-        """
-        Model.__init__(self, name=name, directed=True, multi=multi)
+    def __init__(self, name= 'Unnamed automaton', props=None, multi=False,
+                 init_factory=set, final_factory=set):
+        '''LOMAP Automaton object constructor.'''
+        Model.__init__(self, name=name, directed=True, multi=multi,
+                       init_factory=init_factory, final_factory=final_factory)
 
         if type(props) is dict:
             self.props = dict(props)
@@ -89,28 +89,29 @@ def __repr__(self):
 Edges: {edges}
         '''.format(name=self.name, directed=self.directed, multi=self.multi,
                    props=self.props, alphabet=self.alphabet,
-                   init=list(self.init.keys()), final=self.final,
+                   init=list(self.init), final=self.final,
                    nodes=self.g.nodes(data=True),
                    edges=self.g.edges(data=True))
 
     def clone(self):
-        ret = Automaton(self.name, self.props, self.multi)
+        '''Creates a copy of the automaton.'''
+        aut_class = type(self)
+        ret = aut_class(self.name, self.props, self.multi)
         ret.g = self.g.copy()
-        ret.init = dict(self.init) #FIXME: why is init a dict?
-        ret.final = set(self.final)
+        ret.init = deepcopy(self.init)
+        ret.final = deepcopy(self.final)
+        ret.current = self.current
         return ret
 
     def from_formula(self, formula):
-        """
-        Creates an automaton in-place from the given LTL formula.
-        """
+        '''Creates an automaton in-place from the given LTL formula.'''
         raise NotImplementedError
 
     def get_guard_bitmap(self, guard):
-        """
+        '''
         Creates the bitmaps from guard string. The guard is a boolean expression
         over the atomic propositions.
-        """
+        '''
         # Get sets for all props
         for key in self.props:
             guard = re.sub(r'\b{}\b'.format(key),
@@ -133,50 +134,57 @@ def get_guard_bitmap(self, guard):
         return eval(guard)
 
     def guard_from_bitmaps(self, bitmaps):
-        """
+        '''
         Creates a the guard Boolean formula as a string from the bitmap.
-        """
+        '''
         return '' #TODO: implement
 
     def symbols_w_prop(self, prop):
-        """
+        '''
         Returns symbols from the automaton's alphabet which contain the given
         atomic proposition.
-        """
+        '''
         bitmap = self.props[prop]
         return set([symbol for symbol in self.alphabet if bitmap & symbol])
 
     def symbols_wo_prop(self, prop):
-        """
+        '''
         Returns symbols from the automaton's alphabet which does not contain the
         given atomic proposition.
-        """
+        '''
         return self.alphabet.difference(self.symbols_w_prop(prop))
 
     def bitmap_of_props(self, props):
-        """
+        '''
         Returns bitmap corresponding the set of atomic propositions.
-        """
+        Propositions not in the automaton's proposition set are ignored.
+        '''
         return reduce(op.or_, [self.props.get(p, 0) for p in props], 0)
 
-    def next_states(self, q, props):
-        """
+    def next_states(self, q, props, bitmap=False):
+        '''
         Returns the next states of state q given input proposition set props.
-        """
-        # Get the bitmap representation of props
-        prop_bitmap = self.bitmap_of_props(props)
+        '''
+        if bitmap:
+            prop_bitmap = props
+        else:
+            # Get the bitmap representation of props
+            prop_bitmap = self.bitmap_of_props(props)
         # Return an array of next states
         return [v for _, v, input in self.g.out_edges(q, data='input')
                                                         if prop_bitmap in input]
 
-    def next_state(self, q, props):
+    def next_state(self, q, props, bitmap=False):
         """
         Returns the next state of state q given input proposition set props.
 
         Note: This method should only be used with deterministic automata. It
         might raise an assertion error otherwise.
         """
-        # Get the bitmap representation of props
+        if bitmap:
+            prop_bitmap = props
+        else:
+            # Get the bitmap representation of props
         prop_bitmap = self.bitmap_of_props(props)
         # Return an array of next states
         nq = [v for _, v, input in self.g.out_edges(q, data='input')
@@ -234,14 +242,14 @@ def is_deterministic(self, check_initial=True):
         return True
 
     def add_trap_state(self):
-        """
+        '''
         Adds a trap state and completes the automaton. Returns True whenever a
         trap state has been added to the automaton.
-        """
+        '''
         trap_added = False
         for s in self.g:
             rem_alphabet = set(self.alphabet) \
-                - set(input for _, _, input in self.g.out_edges(s, data='input')
+               - set(input for _, _, input in self.g.out_edges(s, data='input'))
             if rem_alphabet:
                 if not trap_added: #'trap' not in self.g:
                     self.g.add_node('trap')
@@ -290,29 +298,24 @@ def prune(self):
 
 
 class Buchi(Automaton):
-    """
+    '''
     Base class for non-deterministic Buchi automata.
-    """
+    '''
 
     yaml_tag = u'!Buchi'
 
-    def __init__(self, name='Buchi', props=None, multi=True):
-        """
+    def __init__(self, name='Buchi', props=None, multi=False,
+                 init_factory=set, final_factory=set):
+        '''
         LOMAP Buchi Automaton object constructor
-        """
-        Automaton.__init__(self, name=name, props=props, multi=multi)
-
-    def clone(self):
-        ret = Buchi(self.name, self.props, self.multi)
-        ret.g = self.g.copy()
-        ret.init = dict(self.init) #FIXME: why is init a dict?
-        ret.final = set(self.final)
-        return ret
+        '''
+        Automaton.__init__(self, name=name, props=props, multi=multi,
+                           init_factory=init_factory, final_factory=final_factory)
 
     def from_formula(self, formula):
-        """
+        '''
         Creates a Buchi automaton in-place from the given LTL formula.
-        """
+        '''
         try: # Execute ltl2tgba and get output
             lines = sp.check_output(shlex.split(ltl2ba.format(formula=formula))).decode(spot_output_encoding)
         except Exception as ex:
@@ -322,29 +325,24 @@ def from_formula(self, formula):
 
 
 class Fsa(Automaton):
-    """
+    '''
     Base class for (non-)deterministic finite state automata.
-    """
+    '''
 
     yaml_tag = u'!Fsa'
 
-    def __init__(self, name='FSA', props=None, multi=True):
-        """
+    def __init__(self, name='FSA', props=None, multi=False,
+                 init_factory=set, final_factory=set):
+        '''
         LOMAP Fsa Automaton object constructor
-        """
-        Automaton.__init__(self, name=name, props=props, multi=multi)
-
-    def clone(self):
-        ret = Fsa(self.name, self.props, self.multi)
-        ret.g = self.g.copy()
-        ret.init = dict(self.init) #FIXME: why is init a dict?
-        ret.final = set(self.final)
-        return ret
+        '''
+        Automaton.__init__(self, name=name, props=props, multi=multi,
+                           init_factory=init_factory, final_factory=final_factory)
 
     def from_formula(self, formula, load=False):
-        """
+        '''
         Creates a finite state automaton in-place from the given scLTL formula.
-        """
+        '''
         # TODO: check that formula is syntactically co-safe
         try: # Execute ltl2tgba and get output
             lines = sp.check_output(shlex.split(ltl2fsa.format(formula=formula))).decode(spot_output_encoding)
@@ -355,14 +353,14 @@ def from_formula(self, formula, load=False):
         assert(len(self.init)==1)
 
     def is_language_empty(self):
-        """
+        '''
         Checks whether the FSA's language in empty.
-        """
+        '''
         return not any(bool(set(nx.shortest_path(self.g, state)) & self.final)
                        for state in self.init)
 
     def is_word_accepted(self, word, states=None, return_blocking=False):
-        """
+        '''
         Checks whether the input word is accepted by the FSA.
 
         Parameters
@@ -386,7 +384,7 @@ def is_word_accepted(self, word, states=None, return_blocking=False):
         ------
         AssertionError
             If `state` is not a node of the automaton graph.
-        """
+        '''
         if states is None:
             states = self.init
         assert all(state in self.g for state in states)
@@ -416,8 +414,8 @@ def remove_trap_states(self):
         return len(trap_states - set(['virtual'])) == 0
 
     def determinize(self):
-        """
-        Returns a deterministic version of the Buchi automaton.
+        '''
+        Returns a deterministic version of the automaton.
         See page 157 of [1] or [2].
 
 
@@ -425,7 +423,7 @@ def determinize(self):
         Checking. MIT Press, Cambridge, Massachusetts. 2008.
         [2]  John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman. Introduction
         to Automata Theory, Languages, and Computation. Pearson. 2006.
-        """
+        '''
         # Powerset construction
 
         # The new deterministic automaton
@@ -435,8 +433,11 @@ def determinize(self):
         state_map = []
 
         # New initial state
-        state_map.append(set(self.init))
-        det.init[0] = 1
+        init_state = frozenset(self.init)
+        det.init.add(init_state)
+        det.g.add_node(init_state)
+        if init_state & self.final:
+            det.final.add(init_state)
 
         # Copy the old alphabet
         det.alphabet = set(self.alphabet)
@@ -445,67 +446,47 @@ def determinize(self):
         det.props = dict(self.props)
 
         # Discover states and transitions
-        stack = [0]
-        done = set()
+        stack = [init_state]
         while stack:
-            cur_state_i = stack.pop()
-            cur_state_set = state_map[cur_state_i]
-            next_states = dict()
-            for cur_state in cur_state_set:
-                for _,next_state,data in self.g.out_edges_iter(cur_state, True):
-                    inp = next(iter(data['input']))
-                    if inp not in next_states:
-                        next_states[inp] = set()
+            current_state_set = stack.pop()
+            next_states = defaultdict(set)
+            for _, next_state, data in self.g.out_edges(current_state_set, True):
+                for inp in data['input']:
                     next_states[inp].add(next_state)
-
-            for inp,next_state_set in next_states.items():
-                if next_state_set not in state_map:
-                    state_map.append(next_state_set)
-                next_state_i = state_map.index(next_state_set)
-                attr_dict = {'weight':0, 'label':inp, 'input':set([inp])}
-                det.g.add_edge(cur_state_i, next_state_i, **attr_dict)
-                if next_state_i not in done:
-                    stack.append(next_state_i)
-                    done.add(next_state_i)
+            next_states_by_input = defaultdict(set)
+            for inp, next_state_set in next_states.items():
+                key = frozenset(next_state_set)
+                next_states_by_input[key].add(inp)
+                if key not in det.g:
+                    stack.append(key)
+                    # Mark final states
+                    if key & self.final:
+                        det.final.add(key)
+
+            det.g.add_edges_from([
+                (current_state_set, next_state_set, {'input': inps})
+                    for next_state_set, inps in next_states_by_input.items()])
 
         # Sanity check
-        # All edges of all states must be deterministic
-        for state in det.g:
-            ins = set()
-            for _, _, d in det.g.out_edges_iter(state, True):
-                assert len(d['input']) == 1
-                inp = next(iter(d['input']))
-                if inp in ins:
-                    assert False
-                ins.add(inp)
-
-        # Mark final states
-        for state_i, state_set in enumerate(state_map):
-            if state_set & self.final:
-                det.final.add(state_i)
+        assert det.is_deterministic()
 
         return det
 
 
 class Rabin(Automaton):
-    """
+    '''
     Base class for deterministic Rabin automata.
-    """
+    '''
 
     yaml_tag = u'!Rabin'
 
-    def __init__(self, name='Rabin', props=None, multi=True):
+    def __init__(self, name='Rabin', props=None, multi=False,
+                 init_factory=set, final_factory=tuple):
         """
         LOMAP Rabin Automaton object constructor
         """
-        Automaton.__init__(self, name=name, props=props, multi=multi)
-
-    def clone(self):
-        ret = Rabin(self.name, self.props, self.multi)
-        ret.g = self.g.copy()
-        ret.init = dict(self.init) #FIXME: why is init a dict?
-        ret.final = deepcopy(self.final)
-        return ret
+        Automaton.__init__(self, name=name, props=props, multi=multi,
+                           init_factory=init_factory, final_factory=final_factory)
 
     def from_formula(self, formula, prune=False, load=False):
         """
diff --git a/lomap/classes/model.py b/lomap/classes/model.py
index 11a19f4..8359c22 100644
--- a/lomap/classes/model.py
+++ b/lomap/classes/model.py
@@ -47,14 +47,15 @@ class Model(object):
 
     yaml_tag = u'!Model'
 
-    def __init__(self, name='Unnamed model', directed=True, multi=True):
+    def __init__(self, name='Unnamed model', directed=True, multi=False,
+                 init_factory=dict, final_factory=set):
         """
         Empty LOMAP Model object constructor.
         """
         self.name = name
-        self.init = dict()
+        self.init = init_factory()
         self.current = None
-        self.final = set()
+        self.final = final_factory()
         graph_type = graph_constructor(directed, multi)
         self.g = graph_type()
         self.directed = directed
@@ -67,25 +68,23 @@ def __eq__(self, other):
         return (isinstance(other, Model)
             and self.directed == other.directed and self.multi == other.multi
             and self.init == other.init and self.final == other.final
-            #FIXME: Incompatible with nx2.0
-            and nx.graphs_equal(self.g, other.g)
+            and nx.graphs_equal(self.g, other.g))
 
     def __ne__(self, other):
         '''Equality testing. See `Model.__eq__()`.'''
         return not self.__eq__(other)
 
     def nodes_w_prop(self, propset):
-        """
-        Returns the set of nodes with given properties.
-        """
-        return set(node
+        '''Returns the set of nodes with given properties.'''
+        return (node
                     for node, props in self.g.nodes(data='prop', default=set())
-                        if propset <= props))
+                        if propset <= props)
 
     def size(self):
+        '''Returns the number of states and transitions of the model.'''
         return (self.g.number_of_nodes(), self.g.number_of_edges())
 
-    def visualize(self, edgelabel=None, draw='pygraphviz'):
+    def visualize(self, edgelabel=None, draw='matplotlib'):
         """
         Visualizes a LOMAP system model
         """

From ca27fe495120bf9dce4be4cb16c78de87249da02 Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:11:21 -0400
Subject: [PATCH 4/9] Updated interval class.

---
 lomap/classes/interval.py | 25 +++++++++----------------
 1 file changed, 9 insertions(+), 16 deletions(-)

diff --git a/lomap/classes/interval.py b/lomap/classes/interval.py
index b39de0c..4a97999 100644
--- a/lomap/classes/interval.py
+++ b/lomap/classes/interval.py
@@ -77,19 +77,12 @@ def __repr__(self):
         """
         Returns a string representation of an interval object.
         """
-        s = ''
-        if self.closed_start:
-            s += '['
-        else:
-            s += '('
-        s += "%.3f, %.3f" % (self.start, self.end)
-        if self.closed_end:
-            s += ']'
-        else:
-            s += ')'
-        s += ', length: {:.3f}, empty: {}'.format(self.length(),
-                                                  not self.__nonzero__())
-        return s
+        start_par = '[' if self.closed_start else '('
+        stop_par = ']' if self.closed_stop else ')'
+        return '{}{:.3f}, {:.3f}{} , length: {:.3f}, empty: {}'.format(
+                    start_par, self.start, self.stop, stop_par,
+                    self.length(), not self.__nonzero__()
+                )
 
     def __eq__(self, other):
         """
@@ -101,10 +94,10 @@ def __eq__(self, other):
         True
         """
         try:
-            return True if (self.start == other.start and
+            return (self.start == other.start and
                     self.end == other.end and
                     self.closed_start == other.closed_start and
-                    self.closed_end == other.closed_end) else False
+                    self.closed_end == other.closed_end)
         except:
             return False
 
@@ -116,7 +109,7 @@ def __ne__(self, other):
         >>> Interval(0, 0, True, True) != Interval(0, 0, True, False)
         True
         """
-        return False if self.__eq__(other) else True
+        return not self.__eq__(other)
 
     def __neg__(self):
         """

From 8660aef371fbbc2bd0efa30497994d80ddc98472 Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:28:53 -0400
Subject: [PATCH 5/9] Updated system models, Ts and Markov.

---
 lomap/classes/markov.py | 19 ++++++++-----------
 lomap/classes/model.py  |  2 +-
 lomap/classes/ts.py     |  4 ++--
 3 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/lomap/classes/markov.py b/lomap/classes/markov.py
index e4dd2ef..c142530 100644
--- a/lomap/classes/markov.py
+++ b/lomap/classes/markov.py
@@ -1,5 +1,5 @@
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
-#               2015-2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+#               2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -49,7 +49,7 @@ def controls_from_run(self, run):
         for s, t in it.izip(run[:-1], run[1:]):
             # The the third zero index for choosing the first parallel
             # edge in the multidigraph
-            controls.append(self.g[s][t][0].get('control',None))
+            controls.append(self.g[s][t][0].get('control', None))
         return controls
 
     def next_states_of_markov(self, q, traveling_states = True):
@@ -80,7 +80,7 @@ def next_states_of_markov(self, q, traveling_states = True):
         else:
             # q is a normal state of the markov model
             r = []
-            for source, target, data in self.g.out_edges_iter((q,), data=True):
+            for source, target, data in self.g.out_edges((q,), data=True):
                 r.append((target, data['weight'], data.get('control', None), data['prob']))
             return tuple(r)
 
@@ -89,21 +89,18 @@ def iter_action_edges(self, s, a, keys=False):
 
         #FIXME: assumes MultiDiGraph
         '''
-        for _,t,key,d in self.g.out_edges_iter((s,), data=True, keys=True):
+        for _, t, key, d in self.g.out_edges((s,), data=True, keys=True):
             if d['control'] == a:
                 if keys:
-                    yield(t,key,d)
+                    yield(t, key, d)
                 else:
-                    yield (t,d)
+                    yield (t, d)
 
     def available_controls(self, s):
         '''
         Returns all available actions (controls) at the state.
         '''
-        ctrls = set()
-        for _,_,d in self.g.out_edges_iter((s,), data=True):
-            ctrls.add(d['control'])
-        return ctrls
+        return {control for _,_,d in self.g.out_edges((s,), data='control')}
 
     def mc_from_mdp_policy(self, mdp, policy):
         '''
@@ -111,8 +108,8 @@ def mc_from_mdp_policy(self, mdp, policy):
         '''
 
         self.name = 'MC induced on {} by policy'.format(mdp.name)
-        self.init = dict()
         self.final = set()
+
         # Set the initial distribution
         self.init = dict(mdp.init)
 
diff --git a/lomap/classes/model.py b/lomap/classes/model.py
index 8359c22..457b6fa 100644
--- a/lomap/classes/model.py
+++ b/lomap/classes/model.py
@@ -1,5 +1,5 @@
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
-#               2015-2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+#               2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
diff --git a/lomap/classes/ts.py b/lomap/classes/ts.py
index 65d47a7..ff7a568 100644
--- a/lomap/classes/ts.py
+++ b/lomap/classes/ts.py
@@ -1,5 +1,5 @@
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
-#               2015-2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+#               2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -68,7 +68,7 @@ def next_states_of_wts(self, q, traveling_states = True):
         else:
             # q is a normal state of the transition system
             r = []
-            for source, target, data in self.g.edges_iter((q,), data=True):
+            for source, target, data in self.g.edges((q,), data=True):
                 r.append((target, data['weight'], data.get('control', None)))
             return tuple(r)
 

From 08553794b9503f6b53c13891b50f16da9a8017cc Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:30:35 -0400
Subject: [PATCH 6/9] Updated product model contruction methods.

---
 lomap/algorithms/product.py | 422 +++++++++++-------------------------
 1 file changed, 129 insertions(+), 293 deletions(-)

diff --git a/lomap/algorithms/product.py b/lomap/algorithms/product.py
index d2eaf93..12d7cb9 100644
--- a/lomap/algorithms/product.py
+++ b/lomap/algorithms/product.py
@@ -1,7 +1,7 @@
 #! /usr/bin/python
 
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
-#               2016-2017  Cristian-Ioan Vasile (cvasile@mit.edu)
+#               2016-2024  Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -17,8 +17,6 @@
 # with this program; if not, write to the Free Software Foundation, Inc.,
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
-from __future__ import print_function
-
 import itertools as it
 import operator as op
 import logging
@@ -52,7 +50,7 @@ def no_data(*args, **kwargs):
     '''Returns an empty dictionary.'''
     return dict()
 
-def get_default_state_data(state, **kwargs):
+def get_default_state_data(state, c, aut):
     '''Returns the default data to store for a state of a product.
 
     Parameters
@@ -64,10 +62,9 @@ def get_default_state_data(state, **kwargs):
     -------
         dictionary containing the data to be stored.
     '''
-    prop = kwargs.get('prop', None)
-    return {'prop': prop, 'label': "{}\\n{}".format(state, list(prop))}
+    return {'prop': sys.g.nodes[state].get('prop', None)}
 
-def get_default_transition_data(current_state, next_state, **kwargs):
+def get_default_transition_data(current_state, next_state, sys, aut):
     '''Returns the default data to store for a transition of a product.
 
     Parameters
@@ -79,27 +76,42 @@ def get_default_transition_data(current_state, next_state, **kwargs):
     -------
         Dictionary containing the data to be stored.
     '''
-    return {'weight': kwargs.get('weight', None),
-            'control': kwargs.get('control', None)}
+    return {'weight': sys.g[cur_state, next_state].get('weight', None)}
+
+
+def process_product_initial_states(product_model, ts, aut, get_state_data):
+    '''Process the initial states of a product model.
+    
+    Parameters
+    ----------
+    product_model: LOMAP model
+        The product LOMAP model the initial states are added to.
+    
+    ts: LOMAP transition system
 
-def process_product_initial_state(product_model, init_state, get_state_data,
-                                  is_final):
-    '''Process initial product model state.
+    aut: LOMAP automaton
 
-    #TODO: Don't know if this function is useful.
+    get_state_data: function
+        Returns the data to be saved for a state of the product. The function
+        takes the state as a mandatory argument, and no other arguments.
     '''
-    # Add to initial state
-    product_model.init[init_state] = 1
-    # Add to product graph with data
-    init_state_data = get_state_data(init_state)
-    product_model.g.add_node(init_state, **init_state_data)
-    # Check if final
-    if is_final:
-        product_model.final.add(init_state)
+    # Iterate over initial states of the TS
+    for init_ts in ts.init:
+        init_prop = ts.g.nodes[init_ts].get('prop', set())
+        # Iterate over the initial states of the automaton
+        for init_aut in aut.init:
+            # Add the initial states to the product and mark them as initial
+            for act_init_aut in aut.next_states(init_aut, init_prop):
+                init_state = (init_ts, act_init_aut)
+                product_model.init.add(init_state)
+                init_state_data = get_state_data(init_state)
+                product_model.g.add_node(init_state, **init_state_data)
+                if act_init_aut in fsa.final:
+                    product_model.final.add(init_state)
+
 
 def process_product_transition(product_model, stack, current_state, next_state,
-                               blocking, is_final, get_state_data,
-                               get_transition_data):
+                               is_final, get_state_data, get_transition_data):
     '''Process a transition of a product model.
 
     Parameters
@@ -116,9 +128,6 @@ def process_product_transition(product_model, stack, current_state, next_state,
     next_state: hashable
         The destination endpoint state of the transition.
 
-    blocking: Boolean
-        Indicates whether the transition is blocking.
-
     is_final: Boolean
         Indicates whether next_state is an accepting state.
 
@@ -131,39 +140,43 @@ def process_product_transition(product_model, stack, current_state, next_state,
         function takes the two endpoint states as mandatory arguments, and
         no other arguments.
     '''
-    # If no FSA got blocked
-    if not blocking:
-        # form new product automaton state
-        if next_state not in product_model.g:
-            # Add new state with data
-            next_state_data = get_state_data(next_state)
-            product_model.g.add_node(next_state, **next_state_data)
-            # Mark as final if it is final for all FSAs
-            if is_final:
-                product_model.final.add(next_state)
-            # Continue search from next state
-            stack.append(next_state)
-        if next_state not in product_model.g[current_state]:
-            # Add transition with data
-            transition_data = get_transition_data(current_state, next_state)
-            product_model.g.add_edge(current_state, next_state,
-                                     attr_dict=transition_data)
-
-
-def ts_times_fsa(ts, fsa, from_current=False, expand_finals=True,
-                 get_state_data=get_default_state_data,
-                 get_transition_data=get_default_transition_data):
-    '''Computes the product automaton between a transition system and an FSA.
+    # form new product automaton state
+    if next_state not in product_model.g:
+        # Add new state with data
+        next_state_data = get_state_data(next_state)
+        product_model.g.add_node(next_state, **next_state_data)
+        # Mark as final if it is final for all FSAs
+        if is_final:
+            product_model.final.add(next_state)
+        # Continue search from next state
+        stack.append(next_state)
+    if next_state not in product_model.g[current_state]:
+        # Add transition with data
+        transition_data = get_transition_data(current_state, next_state)
+        product_model.g.add_edge(current_state, next_state,
+                                 attr_dict=transition_data)
+
+
+def system_times_automaton(sys, aut, from_current=False, expand_finals=True,
+                           product_type=Model,
+                           get_state_data=get_default_state_data,
+                           get_transition_data=get_default_transition_data):
+    '''Computes the product automaton between a transition system and an
+    automaton.
 
     Parameters
     ----------
-    ts: LOMAP transition system
+    sys: LOMAP system model
 
-    fsa: LOMAP deterministic finite state automaton
+    aut: LOMAP automaton
 
     from_current: bool, optional (default: False)
         Indicates whether the product automaton should be constructed starting
-        from the current TS and FSA states.
+        from the current TS and Automaton states.
+
+    expand_finals: bool, optional (default: True)
+        Indicates whether the product automaton construction should proceed
+        beyond reaching final states.
 
     get_state_data: function, optional (default: get_default_state_data)
         Returns the data to be saved for a state of the product. The function
@@ -182,8 +195,8 @@ def ts_times_fsa(ts, fsa, from_current=False, expand_finals=True,
     Notes
     -----
     The procedure supports only a single current state for construction with
-    the from_current option set. The current state is retrieved from the ts
-    and fsa.
+    the from_current option set. The current state is retrieved from the system
+    model and automaton.
 
     TODO
     ----
@@ -191,146 +204,48 @@ def ts_times_fsa(ts, fsa, from_current=False, expand_finals=True,
     Add debugging logging.
     '''
 
-    # Create the product_model
-    product_model = Model()
+    get_state_data_ = lambda state: get_state_data(state, sys, aut)
+    get_transition_data_ = lambda current_state, next_state: \
+        get_transition_data(current_state, next_state, sys, aut)
+
+    # Create product model
+    multi = sys.multi or aut.multi
+    assert aut.directed
+    product_model = product_type(directed=True, multi=multi,
+                                 init_factory=set, final_factory=set)
+
+    # Process initial states
     if from_current:
-        product_model.init[(ts.current, fsa.current)] = 1
+        product_model.init.add((sys.current, fsa.current))
     else:
-        # Iterate over initial states of the TS
-        for init_ts in ts.init:
-            init_prop = ts.g.node[init_ts].get('prop', set())
-            # Iterate over the initial states of the FSA
-            for init_fsa in fsa.init:
-                # Add the initial states to the graph and mark them as initial
-                act_init_fsa = fsa.next_state(init_fsa, init_prop)
-                if act_init_fsa is not None:
-                    init_state = (init_ts, act_init_fsa)
-                    product_model.init[init_state] = 1
-                    init_state_data = get_state_data(init_state, prop=init_prop,
-                                                     ts=ts, fsa=fsa)
-                    product_model.g.add_node(init_state, **init_state_data)
-                    if act_init_fsa in fsa.final:
-                        product_model.final.add(init_state)
+        process_product_initial_states()
 
     # Add all initial states to the stack
     stack = deque(product_model.init)
     # Consume the stack
     while stack:
-        cur_state = stack.pop()
-        ts_state, fsa_state = cur_state
+        current_state = stack.pop()
+        sys_state, aut_state = current_state
 
         # skip processing final beyond final states
-        if not expand_finals and fsa_state in fsa.final:
+        if not expand_finals and aut_state in aut.final:
             continue
 
-        for ts_next_state, weight, control in ts.next_states_of_wts(ts_state,
-                                                     traveling_states=False):
-            ts_next_prop = ts.g.node[ts_next_state].get('prop', set())
-            fsa_next_state = fsa.next_state(fsa_state, ts_next_prop)
-            if fsa_next_state is not None:
-                # TODO: use process_product_transition instead
-                next_state = (ts_next_state, fsa_next_state)
-                if next_state not in product_model.g:
-                    next_prop = ts.g.node[ts_next_state].get('prop', set())
-                    # Add the new state
-                    next_state_data = get_state_data(next_state, prop=next_prop,
-                                                     ts=ts, fsa=fsa)
-                    product_model.g.add_node(next_state, **next_state_data)
-                    # Add transition w/ data
-                    transition_data = get_transition_data(cur_state, next_state,
-                                weight=weight, control=control, ts=ts, fsa=fsa)
-                    product_model.g.add_edge(cur_state, next_state,
-                                             attr_dict=transition_data)
-                    # Mark as final if final in fsa
-                    if fsa_next_state in fsa.final:
-                        product_model.final.add(next_state)
-                    # Continue search from next state
-                    stack.append(next_state)
-                elif next_state not in product_model.g[cur_state]:
-                    # Add transition w/ data
-                    transition_data = get_transition_data(cur_state, next_state,
-                                weight=weight, control=control, ts=ts, fsa=fsa)
-                    product_model.g.add_edge(cur_state, next_state,
-                                             attr_dict=transition_data)
-
+        for sys_next_state, sys_next_prop in sys.g[ts_state].data('prop', set()):
+            for aut_next_state in aut.next_states(aut_state, sys_next_prop)
+                process_product_transition(
+                    product_model,
+                    stack,
+                    current_state=current_state,
+                    next_state=(sys_next_state, aut_next_state),
+                    is_final=aut_next_state in aut.final,
+                    get_state_data=get_state_data_,
+                    get_transition_data=get_transition_data_
+                )
     return product_model
 
-def ts_times_buchi(ts, buchi):
-    '''TODO:
-    add option to choose what to save on the automaton's
-    add description
-    add regression tests
-    add option to create from current state
-    '''
-
-    # Create the product_model
-    product_model = Model()
-
-    # Iterate over initial states of the TS
-    init_states = []
-    for init_ts in ts.init:
-        init_prop = ts.g.node[init_ts].get('prop',set())
-        # Iterate over the initial states of the FSA
-        for init_buchi in buchi.init:
-            # Add the initial states to the graph and mark them as initial
-            for act_init_buchi in buchi.next_states(init_buchi, init_prop):
-                init_state = (init_ts, act_init_buchi)
-                init_states.append(init_state)
-                product_model.init[init_state] = 1
-                attr_dict = {'prop': init_prop,
-                        'label': '{}\\n{}'.format(init_state,list(init_prop))}
-                product_model.g.add_node(init_state, attr_dict=attr_dict)
-                if act_init_buchi in buchi.final:
-                    product_model.final.add(init_state)
-
-    # Add all initial states to the stack
-    stack = []
-    for init_state in init_states:
-        stack.append(init_state)
-
-    # Consume the stack
-    while(stack):
-        cur_state = stack.pop()
-        ts_state = cur_state[0]
-        buchi_state = cur_state[1]
-
-        for ts_next in ts.next_states_of_wts(ts_state, traveling_states=False):
-            ts_next_state = ts_next[0]
-            ts_next_prop = ts.g.node[ts_next_state].get('prop',set())
-            weight = ts_next[1]
-            control = ts_next[2]
-            for buchi_next_state in buchi.next_states(buchi_state,
-                                                      ts_next_prop):
-                # TODO: use process_product_transition instead
-                next_state = (ts_next_state, buchi_next_state)
-                #print "%s -%d-> %s" % (cur_state, weight, next_state)
-
-                if(next_state not in product_model.g):
-                    next_prop = ts.g.node[ts_next_state].get('prop',set())
-
-                    # Add the new state
-                    attr_dict = {'prop': next_prop,
-                        'label': '{}\\n{}'.format(next_state, list(next_prop))}
-                    product_model.g.add_node(next_state, attr_dict=attr_dict)
-
-                    # Add transition w/ weight
-                    attr_dict = {'weight': weight, 'control': control}
-                    product_model.g.add_edge(cur_state, next_state,
-                                             attr_dict=attr_dict)
-
-                    # Mark as final if final in buchi
-                    if buchi_next_state in buchi.final:
-                        product_model.final.add(next_state)
-
-                    # Continue search from next state
-                    stack.append(next_state)
-
-                elif(next_state not in product_model.g[cur_state]):
-                    attr_dict = {'weight': weight, 'control': control}
-                    product_model.g.add_edge(cur_state, next_state,
-                                             attr_dict=attr_dict)
-
-    return product_model
+ts_times_fsa = ts_times_automaton
+ts_times_buchi = ts_times_automaton
 
 def ts_times_ts(ts_tuple):
     '''TODO:
@@ -342,11 +257,14 @@ def ts_times_ts(ts_tuple):
     # NOTE: We assume deterministic TS
     assert all((len(ts.init) == 1 for ts in ts_tuple))
 
-    # Initial state label is the tuple of initial states' labels
-    product_ts = Ts()
+    multi = any(ts.multi for ts in ts_tuple)
+    directed = any(ts.directed for ts in ts_tuple)
+    product_ts = Ts(directed=directed, multi=multi,
+                    init_factory=set)
 
+    # Initial state label is the tuple of initial states' labels
     init_state = tuple((next(iter(ts.init)) for ts in ts_tuple))
-    product_ts.init[init_state] = 1
+    product_ts.init.add(init_state)
 
     # Props satisfied at init_state is the union of props
     # For each ts, get the prop of init state or empty set
@@ -467,7 +385,7 @@ def fsa_times_fsa(fsa_tuple, from_current=False,
     # union of all atomic proposition sets
     product_props = set.union(*[set(fsa.props) for fsa in fsa_tuple])
     product_fsa = Fsa(product_props, multi=False)
-    product_fsa.init[init_state] = 1
+    product_fsa.init.add(init_state)
 
     symbol_tables = []
     for fsa in fsa_tuple:
@@ -633,39 +551,18 @@ def ts_times_fsas(ts, fsa_tuple, from_current=None, expand_finals=True,
             pfsa_next_state = tuple(fsa.next_state(fsa_state, ts_next_prop)
                         for fsa, fsa_state in zip(fsa_tuple, pfsa_state))
 
-            process_product_transition(product_model, stack,
-                current_state=current_state,
-                next_state=(ts_next_state, pfsa_next_state),
-                blocking=any(s is None for s in pfsa_next_state),
-                is_final=all(s in fsa.final for s, fsa in
-                                          zip(pfsa_next_state, fsa_tuple)),
-                get_state_data=get_state_data_,
-                get_transition_data=get_transition_data_)
-
-#         # If no FSA got blocked
-#         if all([s is not None for s in pfsa_next_state]):
-#             # form new product automaton state
-#             next_state = (ts_next_state, pfsa_next_state)
-#             if next_state not in product_model.g:
-#                 # Add new state with data
-#                 next_state_data = get_state_data(next_state, ts=ts,
-#                                                  fsa_tuple=fsa_tuple)
-#                 product_model.g.add_node(next_state, **next_state_data)
-#                 # Mark as final if it is final for all FSAs
-#                 if all([s in fsa.final for s, fsa in
-#                                      zip(pfsa_next_state, fsa_tuple)]):
-#                     product_model.final.add(next_state)
-#                 # Continue search from next state
-#                 stack.append(next_state)
-#             if next_state not in product_model.g[current_state]:
-#                 # Add transition with data
-#                 transition_data = get_transition_data(current_state,
-#                                      next_state, ts=ts, fsa_tuple=fsa_tuple)
-#                 product_model.g.add_edge(current_state, next_state,
-#                                          attr_dict=transition_data)
+            if all(s is not None for s in pfsa_next_state):
+                process_product_transition(product_model, stack,
+                    current_state=current_state,
+                    next_state=(ts_next_state, pfsa_next_state),
+                    is_final=all(s in fsa.final for s, fsa in
+                                              zip(pfsa_next_state, fsa_tuple)),
+                    get_state_data=get_state_data_,
+                    get_transition_data=get_transition_data_)
 
     return product_model
 
+
 def flatten_tuple(t):
     '''TODO: add description
     add regression tests
@@ -796,7 +693,7 @@ def markov_times_markov(markov_tuple):
     return mdp
 
 
-def markov_times_fsa(markov, fsa):
+def markov_times_fsa(markov, fsa, from_current=False, expand_finals=True):
     '''TODO:
     add option to choose what to save on the automaton's
     add description
@@ -804,80 +701,19 @@ def markov_times_fsa(markov, fsa):
     add option to create from current state
     '''
 
-    # Create the product_model
-    p = Markov()
-    p.name = 'Product of %s and %s' % (markov.name, fsa.name)
-    p.init = {}
-    p.final = set()
-
-    # Stack for depth first search
-    stack = []
-    # Iterate over initial states of the markov model
-    for init_markov in markov.init.keys():
-        init_prop = markov.g.node[init_markov].get('prop',set())
-        # Iterate over the initial states of the FSA
-        for init_fsa in fsa.init.keys():
-            # Add the initial states to the graph and mark them as initial
-            for act_init_fsa in fsa.next_states(init_fsa, init_prop):
-                init_state = (init_markov, act_init_fsa)
-                # Flatten state label
-                flat_init_state = flatten_tuple(init_state)
-                # Probabilities come from the markov model as FSA is deterministic
-                p.init[flat_init_state] = markov.init[init_markov]
-                p.g.add_node(flat_init_state, {'prop': init_prop,
-                        'label':r'{}\n{:.2f}\n{}'.format(flat_init_state,
-                                    p.init[flat_init_state], list(init_prop))})
-                if act_init_fsa in fsa.final:
-                    p.final.add(flat_init_state)
-                # Add this initial state to stack
-                stack.append(init_state)
-
-    # Consume the stack
-    while stack:
-        cur_state = stack.pop()
-        flat_cur_state = flatten_tuple(cur_state)
-        markov_state = cur_state[0]
-        fsa_state = cur_state[1]
-
-        for markov_next in markov.next_states_of_markov(markov_state,
-                                                      traveling_states = False):
-            markov_next_state = markov_next[0]
-            markov_next_prop = markov.g.node[markov_next_state]['prop']
-            weight = markov_next[1]
-            control = markov_next[2]
-            prob = markov_next[3]
-            for fsa_next_state in fsa.next_states(fsa_state,
-                                                         markov_next_prop):
-                next_state = (markov_next_state, fsa_next_state)
-                flat_next_state = flatten_tuple(next_state)
-                #print "%s -%d-> %s" % (cur_state, weight, next_state)
-
-                if flat_next_state not in p.g:
-                    next_prop = markov.g.node[markov_next_state].get('prop',
-                                                                     set())
-
-                    # Add the new state
-                    p.g.add_node(flat_next_state, {'prop': next_prop,
-                                    'label': "{}\\n{}".format(flat_next_state,
-                                                              list(next_prop))})
-
-                    # Add transition w/ weight and prob
-                    p.g.add_edge(flat_cur_state, flat_next_state,
-                                 attr_dict={'weight': weight,
-                                            'control': control,
-                                            'prob': prob})
-
-                    # Mark as final if final in fsa
-                    if fsa_next_state in fsa.final:
-                        p.final.add(flat_next_state)
-
-                    # Continue search from next state
-                    stack.append(next_state)
-
-                elif flat_next_state not in p.g[flat_cur_state]:
-                    p.g.add_edge(flat_cur_state, flat_next_state,
-                                 attr_dict={'weight': weight,
-                                            'control': control,
-                                            'prob': prob})
-
-    return p
+    def get_transition_data_(current_state, next_state): 
+        d = markov.g[current_state, next_state]
+        return {'weight': d.get('weight', 0),
+                'control': d.get('control', 0),
+                'prob': d.get(prob, 0)}
+
+    # Create the product Markov model
+    pmdp = system_times_automaton(markov, aut,
+                                  from_current=from_current,
+                                  expand_finals=expand_finals,
+                                  product_type=Markov,
+                                  get_state_data=get_default_state_data,
+                                  get_transition_data=get_transition_data_)
+    init_dist = dict(((state, markov.init[state[0]]) for state in pmdp.init))
+    pmdp.init = init_dist
+    return pmdp

From d0aace7fed9c7be43016408da9b0e9bc80e4adcd Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:39:05 -0400
Subject: [PATCH 7/9] Initial update of tests.

---
 lomap/tests/__init__.py      |   2 +-
 lomap/tests/test_automata.py |   3 +-
 lomap/tests/test_fsa.py      |  26 ++++---
 lomap/tests/test_products.py |  14 ++--
 lomap/tests/test_srfs.py     |   3 +-
 lomap/tests/test_yaml.py     |   4 +-
 lomap/tests/tmp_test_wfse.py | 132 +++++++++++++++++++++++++++++++++++
 7 files changed, 155 insertions(+), 29 deletions(-)
 create mode 100644 lomap/tests/tmp_test_wfse.py

diff --git a/lomap/tests/__init__.py b/lomap/tests/__init__.py
index 1ff9abe..c99fad9 100644
--- a/lomap/tests/__init__.py
+++ b/lomap/tests/__init__.py
@@ -1,4 +1,4 @@
-# Copyright (C) 2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+# Copyright (C) 2017-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 # 
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
diff --git a/lomap/tests/test_automata.py b/lomap/tests/test_automata.py
index 63adf4c..2104ff3 100644
--- a/lomap/tests/test_automata.py
+++ b/lomap/tests/test_automata.py
@@ -1,4 +1,4 @@
-# Copyright (C) 2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+# Copyright (C) 2017-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -14,7 +14,6 @@
 # with this program; if not, write to the Free Software Foundation, Inc.,
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
-from __future__ import print_function
 
 from lomap.classes import Buchi, Fsa, Rabin
 
diff --git a/lomap/tests/test_fsa.py b/lomap/tests/test_fsa.py
index 93bd23d..6ec9b11 100644
--- a/lomap/tests/test_fsa.py
+++ b/lomap/tests/test_fsa.py
@@ -1,6 +1,6 @@
 #! /usr/bin/python
 
-# Copyright (C) 2020, Cristian-Ioan Vasile (cvasile@lehigh.edu)
+# Copyright (C) 2020-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -16,8 +16,6 @@
 # with this program; if not, write to the Free Software Foundation, Inc.,
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
-from __future__ import print_function
-
 import networkx as nx
 
 from lomap import Fsa, Ts, ts_times_fsa, ts_times_ts
@@ -32,32 +30,32 @@ def construct_fsa():
 
     # add transitions
     inputs = set(fsa.bitmap_of_props(value) for value in [set()])
-    fsa.g.add_edge('s0', 's0', attr_dict={'input': inputs})
+    fsa.g.add_edge('s0', 's0', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value) for value in [set(['a'])])
-    fsa.g.add_edge('s0', 's1', attr_dict={'input': inputs})
+    fsa.g.add_edge('s0', 's1', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value) for value in [set(['b'])])
-    fsa.g.add_edge('s0', 's2', attr_dict={'input': inputs})
+    fsa.g.add_edge('s0', 's2', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value) for value in [set(['a', 'b'])])
-    fsa.g.add_edge('s0', 's3', attr_dict={'input': inputs})
+    fsa.g.add_edge('s0', 's3', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value) for value in [set(), set(['a'])])
-    fsa.g.add_edge('s1', 's1', attr_dict={'input': inputs})
+    fsa.g.add_edge('s1', 's1', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value)
                  for value in [set(['b']), set(['a', 'b'])])
-    fsa.g.add_edge('s1', 's3', attr_dict={'input': inputs})
+    fsa.g.add_edge('s1', 's3', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value) for value in [set(), set(['b'])])
-    fsa.g.add_edge('s2', 's2', attr_dict={'input': inputs})
+    fsa.g.add_edge('s2', 's2', **{'input': inputs})
 
     inputs = set(fsa.bitmap_of_props(value)
                  for value in [set(['a']), set(['a', 'b'])])
-    fsa.g.add_edge('s2', 's3', attr_dict={'input': inputs})
+    fsa.g.add_edge('s2', 's3', **{'input': inputs})
 
-    fsa.g.add_edge('s3', 's3', attr_dict={'input': fsa.alphabet})
+    fsa.g.add_edge('s3', 's3', **{'input': fsa.alphabet})
 
     # set the initial state
     fsa.init['s0'] = 1
@@ -72,8 +70,8 @@ def construct_ts():
 
     ts.init[(1, 1)] = 1
 
-    ts.g.add_node((0, 0), attr_dict={'prop': set(['a'])})
-    ts.g.add_node((3, 2), attr_dict={'prop': set(['b'])})
+    ts.g.add_node((0, 0), **{'prop': set(['a'])})
+    ts.g.add_node((3, 2), **{'prop': set(['b'])})
 
     ts.g.add_edges_from(ts.g.edges(), weight=1)
 
diff --git a/lomap/tests/test_products.py b/lomap/tests/test_products.py
index b06201b..3d9e44a 100644
--- a/lomap/tests/test_products.py
+++ b/lomap/tests/test_products.py
@@ -1,4 +1,4 @@
-# Copyright (C) 2017, Cristian-Ioan Vasile (cvasile@mit.edu)
+# Copyright (C) 2017-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -74,10 +74,10 @@ def test_ts_times_buchi():
     ts.visualize(edgelabel='weight', draw='matplotlib')
     plt.show()
 
-    for u, d in ts.g.nodes_iter(data=True):
+    for u, d in ts.g.nodes(data=True):
         print(u, d)
     print()
-    for u, v, d in ts.g.edges_iter(data=True):
+    for u, v, d in ts.g.edges(data=True):
         print(u, v, d)
 
     spec = 'G (F a && F g && !e)'
@@ -88,10 +88,10 @@ def test_ts_times_buchi():
     plt.show()
 
     print()
-    for u, d in buchi.g.nodes_iter(data=True):
+    for u, d in buchi.g.nodes(data=True):
         print(u, d)
     print()
-    for u, v, d in buchi.g.edges_iter(data=True):
+    for u, v, d in buchi.g.edges(data=True):
         print(u, v, d)
 
     pa = ts_times_buchi(ts, buchi)
@@ -100,10 +100,10 @@ def test_ts_times_buchi():
     plt.show()
 
     print()
-    for u, d in pa.g.nodes_iter(data=True):
+    for u, d in pa.g.nodes(data=True):
         print(u, d)
     print()
-    for u, v, d in pa.g.edges_iter(data=True):
+    for u, v, d in pa.g.edges(data=True):
         print(u, v, d)
 
     cost, prefix, suffix = policy_buchi_pa(pa)
diff --git a/lomap/tests/test_srfs.py b/lomap/tests/test_srfs.py
index 8dfa3c4..db948f5 100644
--- a/lomap/tests/test_srfs.py
+++ b/lomap/tests/test_srfs.py
@@ -1,6 +1,6 @@
 #! /usr/bin/python
 
-# Copyright (C) 2015-2017, Cristian-Ioan Vasile (cvasile@bu.edu)
+# Copyright (C) 2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -16,7 +16,6 @@
 # with this program; if not, write to the Free Software Foundation, Inc.,
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
-from __future__ import print_function
 
 from collections import defaultdict
 from random import randint, seed
diff --git a/lomap/tests/test_yaml.py b/lomap/tests/test_yaml.py
index c4c6a77..873007c 100644
--- a/lomap/tests/test_yaml.py
+++ b/lomap/tests/test_yaml.py
@@ -1,4 +1,4 @@
-# Copyright (C) 2018, Cristian-Ioan Vasile (cvasile@bu.edu)
+# Copyright (C) 2018-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 #
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -14,8 +14,6 @@
 # with this program; if not, write to the Free Software Foundation, Inc.,
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
-from __future__ import print_function
-
 import random
 import os
 import tempfile
diff --git a/lomap/tests/tmp_test_wfse.py b/lomap/tests/tmp_test_wfse.py
new file mode 100644
index 0000000..1ababfe
--- /dev/null
+++ b/lomap/tests/tmp_test_wfse.py
@@ -0,0 +1,132 @@
+#! /usr/bin/python
+
+# Implementing a test case similar to test_fsa.py
+
+import networkx as nx
+
+from lomap import Fsa, Ts, Wfse, ts_times_wfse_times_fsa
+
+
+def fsa_constructor():
+    ap = set(['a', 'b']) # set of atomic propositions
+    fsa = Fsa(props=ap, multi=False) # empty FSA with propsitions from `ap`
+    # add states
+    fsa.g.add_nodes_from(['s0', 's1', 's2', 's3'])
+
+    #add transitions
+    inputs = set(fsa.bitmap_of_props(value) for value in [set()])
+    fsa.g.add_edge('s0', 's0', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value) for value in [set(['a'])])
+    fsa.g.add_edge('s0', 's1', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value) for value in [set(['b'])])
+    fsa.g.add_edge('s0', 's2', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value) for value in [set(['a', 'b'])])
+    fsa.g.add_edge('s0', 's3', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value) for value in [set(), set(['a'])])
+    fsa.g.add_edge('s1', 's1', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value)
+                 for value in [set(['b']), set(['a', 'b'])])
+    fsa.g.add_edge('s1', 's3', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value) for value in [set(), set(['b'])])
+    fsa.g.add_edge('s2', 's2', attr_dict={'input': inputs})
+    inputs = set(fsa.bitmap_of_props(value)
+                 for value in [set(['a']), set(['a', 'b'])])
+    fsa.g.add_edge('s2', 's3', attr_dict={'input': inputs})
+    fsa.g.add_edge('s3', 's3', attr_dict={'input': fsa.alphabet})
+    # set the initial state
+    fsa.init['s0'] = 1
+    # add `s3` to set of final/accepting states
+    fsa.final.add('s3')
+
+    return fsa
+
+
+def ts_constructor():
+    ts = Ts(directed=True, multi=False)
+    ts.g = nx.grid_2d_graph(4, 3)
+
+    ts.init[(1, 1)] = 1
+
+    ts.g.add_node((0, 0), attr_dict={'prop': set(['a'])})
+    # ts.g.add_node((3, 2), attr_dict={'prop': set(['b'])})
+    ts.g.add_node((3, 2), attr_dict={'prop': set(['c'])})
+
+    ts.g.add_edges_from(ts.g.edges(), weight=1)
+
+    return ts
+
+
+def wfse_constructor():
+    ap = set(['a', 'b', 'c']) # set of atomic propositions
+    wfse = Wfse(props=ap, multi=False)
+    wfse.init = set() # HACK
+
+    # add states
+    wfse.g.add_nodes_from(['q0'])
+
+    # add transitions
+    in_symbol = wfse.bitmap_of_props(set('c'))
+    out_symbol = wfse.bitmap_of_props(set('b'))
+
+    weighted_symbols = [(in_symbol, out_symbol, 2)]
+    for symbol in wfse.prop_bitmaps:
+        if symbol >= 0:
+            weighted_symbols.append((symbol, symbol, 1))
+    print('weighted_symbols:', weighted_symbols)
+    wfse.g.add_edge('q0', 'q0', attr_dict={'symbols': weighted_symbols})
+
+    # set the initial state
+    wfse.init.add('q0')
+
+    return wfse
+
+def main():
+    fsa = fsa_constructor()
+    print(fsa)
+    ts = ts_constructor()
+    print(ts)
+    wfse = wfse_constructor()
+    print(wfse)
+
+    product_model = ts_times_wfse_times_fsa(ts, wfse, fsa)
+    print(product_model)
+
+    print('Product: Init:', product_model.init) # initial states
+    print('Product: Final:', product_model.final) # final states
+
+    # get initial state in product model -- should be only one
+    pa_initial_state = next(iter(product_model.init))
+    # compute shortest path lengths from initial state to all other states
+    lengths = nx.shortest_path_length(product_model.g, source=pa_initial_state)
+    # keep path lenghts only for final states in the product model
+    lengths = {final_state: lengths[final_state]
+               for final_state in product_model.final}
+    # find the final state with minimum length
+    pa_optimal_final_state = min(lengths, key=lengths.get)
+    print('Product: Optimal Final State:', pa_optimal_final_state)
+    # get optimal solution path in product model from initial state to optimal
+    # final state
+    pa_optimal_path = nx.shortest_path(product_model.g, source=pa_initial_state,
+                                       target=pa_optimal_final_state)
+    print('Product: Optimal trajectory:', pa_optimal_path)
+    # get optimal solution path in the transition system (robot motion model)
+    ts_optimal_path, wfse_state_path, fsa_state_path = zip(*pa_optimal_path)
+    print('TS: Optimal Trajectory:', ts_optimal_path)
+    print('WFSE: Optimal Trajectory:', wfse_state_path)
+    print('FSA: Optimal Trajectory:', fsa_state_path)
+
+    print('Symbol translations:')
+    for ts_state, state, next_state in zip(ts_optimal_path[1:], pa_optimal_path,
+                                           pa_optimal_path[1:]):
+        print(ts_state, '->', product_model.g[state][next_state]['prop'])
+
+    # MODIFY HERE // IN PROGRESS
+
+    # Important questions for the next move:
+    # I need to figure out what the wfse constructor outputs
+    # I need to figure out how to extract the corrected path
+    # To do that I will use the functions from product_wfse
+    # I will print the corrected/alternate/substiture path
+
+if __name__ == '__main__':
+    main()

From 7c80fda9a2dd11571f653da50be601b6f2a48542 Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:47:29 -0400
Subject: [PATCH 8/9] Updated the changes log.

---
 CHANGES.md | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 13444b3..76e94f5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,24 @@
+Version 0.1.3 notes and API changes
+
+This page reflects API changes from LOMAP 0.1.2 to NetworkX 3.4.
+Note: The original code written by Alphan Ulusoy has version number 0.1.1.
+
+API changes
+- Automata attribute `init` is now a set by default.
+- Models and automata are created as (di)graphs by default instead of
+multi-(di)graphs.
+- Rabin automata `final` attribute is now a tuple.
+- Added `init_factory` and `final_factory` as arguments of the constructor of
+model, automata, and system classes.
+- Changed output of `nodes_w_prop` method to iterable instead of set.
+- Changed default visualization to `matplotlib` and disabled `pygraphviz`.
+- Added `bitmap` argument to `next_state` and `next_states` of Automaton class
+to select whether the input is a set of APs or a bitmap encoding. The default
+value is false for backwards compatibility.
+- Refactored the `clone` method of Automata. It was removed from Buchi, Fsa,
+and Rabin classes.
+
+
 Version 0.1.2 notes and API changes
 
 This page reflects API changes from LOMAP 0.1.1 to NetworkX 0.1.2.

From 80b57464965907e65bae0f380a760dba7409347d Mon Sep 17 00:00:00 2001
From: Cristian Vasile <cvasile@mit.edu>
Date: Tue, 22 Oct 2024 20:47:59 -0400
Subject: [PATCH 9/9] Bumped the version to 0.1.3.

---
 lomap/__init__.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lomap/__init__.py b/lomap/__init__.py
index 68e7b68..537dcad 100644
--- a/lomap/__init__.py
+++ b/lomap/__init__.py
@@ -1,4 +1,5 @@
 # Copyright (C) 2012-2015, Alphan Ulusoy (alphan@bu.edu)
+# Copyright (C) 2015-2024, Cristian-Ioan Vasile (cvasile@lehigh.edu)
 # 
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -26,4 +27,4 @@
 from .algorithms.srfs import *
 from .classes.automata import spot_output_encoding, ltl2dstar_output_encoding
 
-__version__ = (0, 1, 2)
+__version__ = (0, 1, 3)