show how to implement product in Python

* wrap/python/tests/product.ipynb: New file.
* wrap/python/tests/Makefile.am, doc/org/tut.org: Add it.
* wrap/python/tests/ipnbdoctest.py: Ignore %timeit results.
* wrap/python/spot_impl.i: Add bindings for
set_state_names()/get_state_names().
* spot/twaalgos/product.cc: Fix computation of properties.
* doc/org/hoa.org: Name.
* NEWS: Update.

NEWS

@@ -64,15 +64,25 @@ New in spot 1.99.6a (not yet released)
     when calling for instance the Python version of twa_graph::new_edge().
     See https://spot.lrde.epita.fr/tut22.html for a demonstration.
 
+  * Automaton states can be named via the set_state_names() method.
+    See https://spot.lrde.epita.fr/ipynb/product.html for an example.
+
   Documentation:
 
   * There is a new page explaining how to compile example programs and
     and link them with Spot.  https://spot.lrde.epita.fr/compile.html
 
+  * Python bindings for manipulating acceptance conditions are
+    demonstrated by https://spot.lrde.epita.fr/ipynb/acc_cond.html,
+    and a Python implementation of the product of two automata is
+    illustrated by https://spot.lrde.epita.fr/ipynb/product.html
+
   Bug fixes:
 
   * twa::ap() would contain duplicates when an atomic proposition
     was registered several times.
+  * product() would incorrectly mark the product of two
+    sttuter-sensitive automata as stutter-sensitive as well.
 
 New in spot 1.99.6 (2015-12-04)
 

doc/org/hoa.org

@@ -584,6 +584,9 @@ labels whenever that is possible.  The option is named =k= (i.e., use
 is used to describe a Kripke structure.
 
 ** Property bits
+   :PROPERTIES:
+   :CUSTOM_ID: property-bits
+   :END:
 
 The =HOA= format supports a number of optional =property:= tokens.
 These properties can be useful to speedup certain algorithms: for

doc/org/tut.org

@@ -52,6 +52,8 @@ real notebooks instead.
 - [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser
 - [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][acc_cond.ipynb]] documents the interface for manipulating acceptance
   conditions
+- [[https://spot.lrde.epita.fr/ipynb/product.html][product.ipynb]] shows how to re-implement the product of two automata
+  in Python
 - [[https://spot.lrde.epita.fr/ipynb/randltl.html][randltl.ipynb]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
 - [[https://spot.lrde.epita.fr/ipynb/decompose.html][decompose.ipynb]] illustrates the =decompose_strength()= function
 - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing

spot/twaalgos/product.cc

@@ -105,10 +105,18 @@ namespace spot
 			      && right->prop_deterministic());
       res->prop_stutter_invariant(left->prop_stutter_invariant()
 				  && right->prop_stutter_invariant());
-      res->prop_stutter_sensitive(left->prop_stutter_sensitive()
-				  && right->prop_stutter_sensitive());
+      // The product of X!a and Xa, two stutter-sentive formulas,
+      // is stutter-invariant.
+      //res->prop_stutter_sensitive(left->prop_stutter_sensitive()
+      //			    && right->prop_stutter_sensitive());
+      res->prop_inherently_weak(left->prop_inherently_weak()
+				&& right->prop_inherently_weak());
+      res->prop_weak(left->prop_weak()
+		     && right->prop_weak());
+      res->prop_terminal(left->prop_terminal()
+			 && right->prop_terminal());
       res->prop_state_acc(left->prop_state_acc()
-				&& right->prop_state_acc());
+			  && right->prop_state_acc());
       return res;
     }
   }

wrap/python/spot_impl.i

@@ -339,6 +339,7 @@ namespace std {
   %template(liststr) list<std::string>;
   %template(vectorformula) vector<spot::formula>;
   %template(vectorunsigned) vector<unsigned>;
+  %template(vectorstring) vector<string>;
   %template(atomic_prop_set) set<spot::formula>;
   %template(relabeling_map) map<spot::formula, spot::formula>;
 }
@@ -465,6 +466,18 @@ namespace std {
   std::string __str__() { return spot::str_psl(*self); }
 }
 
+%extend spot::bdd_dict {
+  bool operator==(const spot::bdd_dict& b) const
+  {
+    return self == &b;
+  }
+
+  bool operator!=(const spot::bdd_dict& b) const
+  {
+    return self != &b;
+  }
+}
+
 %extend spot::twa {
   void set_name(std::string name)
   {
@@ -475,6 +488,17 @@ namespace std {
   {
     return self->get_named_prop<std::string>("automaton-name");
   }
+
+  void set_state_names(std::vector<std::string> names)
+  {
+    self->set_named_prop("state-names",
+			 new std::vector<std::string>(std::move(names)));
+  }
+
+  std::vector<std::string>* get_state_names()
+  {
+    return self->get_named_prop<std::vector<std::string>>("state-names");
+  }
 }
 
 

wrap/python/tests/Makefile.am

@@ -49,6 +49,7 @@ TESTS = \
   optionmap.py \
   parsetgba.py \
   piperead.ipynb \
+  product.ipynb \
   randaut.ipynb \
   randgen.py \
   randltl.ipynb \

wrap/python/tests/ipnbdoctest.py

@@ -70,6 +70,9 @@ def sanitize(s):
     # normalize graphviz version
     s = re.sub(r'Generated by graphviz version.*', 'VERSION', s)
 
+    # ignore %timeit results
+    s = re.sub(r'^[0-9]+ loops, best of 3:.*per loop', '', s)
+
     # SVG generated by graphviz may put note at different positions
     # depending on the graphviz build.  Let's just strip anything that
     # look like a position.