Parse HOA AP header

regression/ebmc-spot/ltl-buechi/implies3.desc

@@ -0,0 +1,8 @@
+CORE
+implies3.smv
+--buechi --bound 5
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/implies3.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC ! (F x = 1 -> F x = 0) -- should pass

regression/ebmc-spot/sva-buechi/if1.k.desc

@@ -1,6 +1,6 @@
 CORE
 ../../verilog/SVA/if1.sv
---buechi --k-induction --bound 1
+--buechi --k-induction --bound 2
 ^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED$
 ^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sequence_and1.sv
+--buechi --bdd
+^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
+^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
+^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED$
+^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED$
+^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sequence_and1.sv
+--buechi --bound 5
+^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
+^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
+^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED up to bound \d+$
+^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED up to bound \d+$
+^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

src/temporal-logic/hoa.cpp

@@ -266,6 +266,28 @@ hoat::headert hoa_parsert::parse_header()
   return header;
 }
 
+hoat::ap_mapt hoat::parse_AP() const
+{
+  for(auto &item : header)
+  {
+    if(item.first == "AP:")
+    {
+      hoat::ap_mapt result;
+      std::size_t index = 0;
+      for(auto &name : item.second)
+      {
+        if(index != 0)
+          result[index - 1] = name;
+        index++;
+      }
+      return result;
+    }
+  }
+
+  // header not found
+  return {};
+}
+
 hoat::bodyt hoa_parsert::parse_body()
 {
   if(!tokenizer.consume().is_body())
@@ -323,8 +345,6 @@ hoat::edgest hoa_parsert::parse_edges()
   return edges;
 }
 
-#include <iostream>
-
 hoat::edget hoa_parsert::parse_edge()
 {
   edget edge;

src/temporal-logic/hoa.h

@@ -68,7 +68,10 @@ class hoat
   intt max_state_number() const;
 
   // atomic propositions
-  std::map<intt, std::string> ap_map;
+  using ap_mapt = std::map<intt, std::string>;
+
+  // parses the AP header
+  ap_mapt parse_AP() const;
 
   // convert into a graph
   struct graph_edget

src/temporal-logic/ltl_sva_to_string.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/arith_tools.h>
 #include <util/string2int.h>
 
+#include <ebmc/ebmc_error.h>
 #include <verilog/sva_expr.h>
 
 #include "ltl.h"
@@ -21,8 +22,11 @@ Author: Daniel Kroening, dkr@amazon.com
 
 exprt ltl_sva_to_stringt::atom(const std::string &string) const
 {
+  if(string.empty() || string[0] != 'a')
+    throw ebmc_errort{} << "got unexpected atom '" << string << "'";
+
   // map back to number
-  auto number = safe_string2size_t(string);
+  auto number = safe_string2size_t(string.substr(1, std::string::npos));
 
   PRECONDITION(number < atoms.size());
 

src/temporal-logic/ltl_sva_to_string.h

@@ -53,6 +53,8 @@ class ltl_sva_to_stringt
     std::string s;
   };
 
+  // This maps our expressions to a number.
+  // Spot may or may not use the same numbering in the AP header.
   numberingt<exprt, irep_hash> atoms;
 
   using modet = enum { PROPERTY, SVA_SEQUENCE, BOOLEAN };

src/temporal-logic/ltl_to_buechi.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/run.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/string2int.h>
 
 #include <ebmc/ebmc_error.h>
 #include <trans-word-level/next_symbol.h>
@@ -46,12 +47,13 @@ void buechi_transt::rename_state_symbol(const symbol_exprt &new_state_symbol)
 
 exprt hoa_label_to_expr(
   const hoat::labelt &label,
-  const ltl_sva_to_stringt &ltl_sva_to_string)
+  const ltl_sva_to_stringt &ltl_sva_to_string,
+  const hoat::ap_mapt &ap_map)
 {
   std::vector<exprt> operands;
   operands.reserve(label.get_sub().size());
   for(auto &sub : label.get_sub())
-    operands.push_back(hoa_label_to_expr(sub, ltl_sva_to_string));
+    operands.push_back(hoa_label_to_expr(sub, ltl_sva_to_string, ap_map));
 
   if(label.id() == "t")
   {
@@ -78,8 +80,17 @@ exprt hoa_label_to_expr(
   }
   else
   {
-    // atomic proposition, given as number
-    return ltl_sva_to_string.atom(label.id_string());
+    // Atomic proposition, given as number. This is the numbering
+    // from the "AP" header, which then maps to a string "aX", which
+    // is our atom number.  These may or may not match.
+    auto spot_ap_number = safe_string2size_t(label.id_string());
+
+    auto ap_map_it = ap_map.find(spot_ap_number);
+    if(ap_map_it == ap_map.end())
+      throw ebmc_errort{} << "failed to find atom " << label.id()
+                          << " in AP header";
+
+    return ltl_sva_to_string.atom(ap_map_it->second);
   }
 }
 
@@ -150,6 +161,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
     hoa.buechi_acceptance_cleanup();
 
     auto max_state_number = hoa.max_state_number();
+    auto ap_map = hoa.parse_AP();
     auto state_type = range_typet{0, max_state_number};
     const auto buechi_state = symbol_exprt{"buechi::state", state_type};
     const auto buechi_next_state =
@@ -220,7 +232,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
         {
           auto pre = equal_exprt{
             buechi_state, from_integer(state.first.number, state_type)};
-          auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string);
+          auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string, ap_map);
           error_disjuncts.push_back(and_exprt{pre, cond});
         }
       }
@@ -242,7 +254,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
       {
         if(edge.dest_states.size() != 1)
           throw ebmc_errort() << "edge must have one destination state";
-        auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string);
+        auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string, ap_map);
         auto post = equal_exprt{
           buechi_next_state,
           from_integer(edge.dest_states.front(), state_type)};