From 78add1d44bcab357ae76b352137b13e1eadbdb78 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 30 May 2017 18:04:57 +0200
Subject: [PATCH] acc: add a maybe_accepting() method

* spot/twa/acc.cc, spot/twa/acc.hh: Implement the new method, and
use it to implement inf_accepting().
* tests/python/accparse2.py: Add some tests.
---
 spot/twa/acc.cc           | 45 ++++++++++++++++++++++++++++-----------
 spot/twa/acc.hh           | 10 +++++++++
 tests/python/accparse2.py | 12 ++++++++++-
 3 files changed, 54 insertions(+), 13 deletions(-)

diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index be535329b..16c43b261 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -215,39 +215,52 @@ namespace spot
       return false;
     }
 
-    static bool
-    inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
+    static trival
+    partial_eval(acc_cond::mark_t infinitely_often,
+                 acc_cond::mark_t always_present,
+                 const acc_cond::acc_word* pos)
     {
       switch (pos->sub.op)
         {
         case acc_cond::acc_op::And:
           {
             auto sub = pos - pos->sub.size;
+            trival res = true;
             while (sub < pos)
               {
                 --pos;
-                if (!inf_eval(inf, pos))
-                  return false;
+                res = res &&
+                  partial_eval(infinitely_often, always_present, pos);
+                if (res.is_false())
+                  return res;
                 pos -= pos->sub.size;
               }
-            return true;
+            return res;
           }
         case acc_cond::acc_op::Or:
           {
             auto sub = pos - pos->sub.size;
+            trival res = false;
             while (sub < pos)
               {
                 --pos;
-                if (inf_eval(inf, pos))
-                  return true;
+                res = res ||
+                  partial_eval(infinitely_often, always_present, pos);
+                if (res.is_true())
+                  return res;
                 pos -= pos->sub.size;
               }
-            return false;
+            return res;
           }
         case acc_cond::acc_op::Inf:
-          return (pos[-1].mark & inf) == pos[-1].mark;
+          return (pos[-1].mark & infinitely_often) == pos[-1].mark;
         case acc_cond::acc_op::Fin:
-          return true;
+          if (pos[-1].mark & always_present)
+            return false;
+          else if (pos[-1].mark & infinitely_often)
+            return trival::maybe();
+          else
+            return true;
         case acc_cond::acc_op::FinNeg:
         case acc_cond::acc_op::InfNeg:
           SPOT_UNREACHABLE();
@@ -310,13 +323,21 @@ namespace spot
     return eval(inf, &back());
   }
 
-  bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const
+  trival acc_cond::acc_code::maybe_accepting(mark_t infinitely_often,
+                                             mark_t always_present) const
   {
     if (empty())
       return true;
-    return inf_eval(inf, &back());
+    return partial_eval(infinitely_often | always_present,
+                        always_present, &back());
   }
 
+  bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const
+  {
+    return !maybe_accepting(inf, 0U).is_false();
+  }
+
+
   acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const
   {
     if (uses_fin_acceptance())
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index 03ea824fd..caa3000a7 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -24,6 +24,7 @@
 #include <sstream>
 #include <vector>
 #include <spot/tl/defaultenv.hh>
+#include <spot/misc/trival.hh>
 #include <iostream>
 
 namespace spot
@@ -888,6 +889,10 @@ namespace spot
 
       bool inf_satisfiable(mark_t inf) const;
 
+      trival maybe_accepting(mark_t infinitely_often,
+                             mark_t always_present) const;
+
+
       // Remove all the acceptance sets in rem.
       //
       // If MISSING is set, the acceptance sets are assumed to be
@@ -1238,6 +1243,11 @@ namespace spot
       return code_.inf_satisfiable(inf);
     }
 
+    trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
+    {
+      return code_.maybe_accepting(infinitely_often, always_present);
+    }
+
     mark_t accepting_sets(mark_t inf) const;
 
     std::ostream& format(std::ostream& os, mark_t m) const
diff --git a/tests/python/accparse2.py b/tests/python/accparse2.py
index 3bcf6a96e..48c8d66e1 100644
--- a/tests/python/accparse2.py
+++ b/tests/python/accparse2.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015  Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2017  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -31,6 +31,16 @@ a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')
 assert(a.is_parity()[0] == False)
 assert(a.is_parity(True) == [True, True, False])
 
+assert a.maybe_accepting([1, 2, 3], [0, 4]).is_true()
+assert a.maybe_accepting([0], []).is_true()
+assert a.maybe_accepting([0], [3]).is_false()
+assert a.maybe_accepting([0, 3], []).is_maybe()
+assert a.maybe_accepting([2, 3], [3]).is_false()
+assert a.maybe_accepting([2, 3], []).is_maybe()
+assert a.maybe_accepting([2], []).is_true()
+assert a.maybe_accepting([0, 1], []).is_maybe()
+assert a.maybe_accepting([0, 1], [1]).is_false()
+
 a = spot.acc_cond(0)
 a.set_acceptance('all')
 assert(a.is_rabin() == -1)