Fix predicates + following_sibling/self + add self in Formula.st + use it in Run

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index fff387a..5d6580a 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -165,7 +165,7 @@ let rec tp_max asta run tree tnode =
       (* compute states occuring in transition candidates *)
       let rec add_st (ql,qr) = function
         | [] -> ql,qr
-        | f :: tl -> let sql,sqr = Formula.st f in
+        | f :: tl -> let sqs,sql,sqr = Formula.st f in
                      let ql' = StateSet.union sql ql
                      and qr' = StateSet.union sqr qr in
                      add_st (ql',qr') tl in