Merge pull request #1129 from diffblue/more-buechi

SVA-to-Buechi: `#-#` and `#=#`

Author: tautschnig

regression/ebmc-spot/sva-buechi/followed-by1.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by1.sv
+--buechi --bdd
+^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): PROVED$
+^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by1.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by1.sv
+--buechi --bound 20 --numbered-trace
+^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): PROVED up to bound 20$
+^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by2.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by2.sv
+--buechi --bdd
+^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): PROVED$
+^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by2.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by2.sv
+--buechi --bound 20
+^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): PROVED up to bound 20$
+^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by3.desc

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/followed-by3.sv
+--buechi --bound 20
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #-# \(s_eventually main\.x == 10\): PROVED up to bound 20$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #=# \(s_eventually main\.x == 10\): PROVED up to bound 20$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #-# \(s_eventually main\.x == 2\): PROVED up to bound 20$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #-# \(s_eventually main\.x == 11\): REFUTED$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #=# \(s_eventually main\.x == 1\): REFUTED$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 2\) #-# 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by4.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/followed-by4.sv
+--buechi --bdd
+^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
+^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: PROVED$
+^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+../../verilog/SVA/followed-by4.sv
+--buechi --bound 3
+^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
+^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: PROVED up to bound 3$
+^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: PROVED up to bound 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+p1 is not refuted.

src/temporal-logic/ltl_sva_to_string.cpp

@@ -233,12 +233,29 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
       ID_sva_implicit_weak, new_expr.sequence()};
     return infix("|=>", new_expr, mode);
   }
-  else if(
-    expr.id() == ID_sva_nonoverlapped_followed_by ||
-    expr.id() == ID_sva_overlapped_followed_by)
+  else if(expr.id() == ID_sva_overlapped_followed_by)
   {
     PRECONDITION(mode == PROPERTY);
-    throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi";
+    // 1800 2017 16.12.9
+    // (a #-# b)   --->   !(a |-> !b)
+    auto &followed_by = to_sva_followed_by_expr(expr);
+    auto not_b = not_exprt{followed_by.consequent()};
+    return rec(
+      not_exprt{
+        sva_overlapped_implication_exprt{followed_by.antecedent(), not_b}},
+      mode);
+  }
+  else if(expr.id() == ID_sva_nonoverlapped_followed_by)
+  {
+    PRECONDITION(mode == PROPERTY);
+    // 1800 2017 16.12.9
+    // (a #=# b)   --->   !(a |=> !b)
+    auto &followed_by = to_sva_followed_by_expr(expr);
+    auto not_b = not_exprt{followed_by.consequent()};
+    return rec(
+      not_exprt{
+        sva_non_overlapped_implication_exprt{followed_by.antecedent(), not_b}},
+      mode);
   }
   else if(expr.id() == ID_sva_sequence_property)
   {