Merge pull request #369 from diffblue/numbered-trace

ebmc: traces with identifiers numbered with time frames

Author: tautschnig

regression/ebmc/traces/numbered1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+waveform1.smv
+--bound 20 --numbered-trace
+^EXIT=10$
+^SIGNAL=0$
+^\[smv::main::spec1\] .* REFUTED$
+^Counterexample:$
+^smv::main::var::y@0 = 0$
+^smv::main::var::y@10 = 100$
+^smv::main::var::y@20 = 200$
+--
+^warning: ignoring

regression/ebmc/traces/numbered1.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x: 0..20;
+VAR y: 0..200;
+VAR z: 0..20;
+
+INIT x=0
+INIT y=0
+INIT z=0
+
+ASSIGN next(x):=x + 1;
+ASSIGN next(y):=y + 10;
+ASSIGN next(z):=z;
+
+SPEC AG x!=20

src/ebmc/ebmc_parse_options.cpp

@@ -359,6 +359,7 @@ void ebmc_parse_optionst::help()
     " {y--trace}                     \t generate a trace for failing properties\n"
     " {y--vcd} {ufile name}          \t generate traces in VCD format\n"
     " {y--waveform}                  \t show a waveform for failing properties\n"
+    " {y--numbered-trace}            \t give a trace with identifiers numbered by timeframe\n"
     " {y--show-properties}           \t list the properties in the model\n"
     " {y--property} {uid}            \t check the property with given ID\n"
     " {y-I} {upath}                  \t set include path\n"

src/ebmc/ebmc_parse_options.h

@@ -28,7 +28,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(show-ldg)(show-modules)(show-module-hierarchy)"
         "(show-trans)(show-bdds)(show-formula)"
         "(modules-xml):"
-        "(show-properties)(property):p:(trace)(waveform)"
+        "(show-properties)(property):p:(trace)(waveform)(numbered-trace)"
         "(dimacs)(module):(top):"
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)(json-result):"

src/ebmc/random_traces.cpp

@@ -179,6 +179,12 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
       consolet::out() << "*** Trace " << (trace_nr + 1) << '\n';
       show_waveform(trace, ns);
     }
+    else if(cmdline.isset("numbered-trace"))
+    {
+      consolet::out() << "*** Trace " << (trace_nr + 1) << '\n';
+      messaget message(message_handler);
+      show_trans_trace_numbered(trace, message, ns, consolet::out());
+    }
     else // default
     {
       consolet::out() << "*** Trace " << (trace_nr + 1) << '\n';

src/ebmc/report_results.cpp

@@ -129,6 +129,12 @@ void report_results(
           show_trans_trace(
             property.counterexample.value(), message, ns, std::cout);
         }
+        else if(cmdline.isset("numbered-trace"))
+        {
+          message.status() << "Counterexample:\n" << messaget::eom;
+          show_trans_trace_numbered(
+            property.counterexample.value(), message, ns, std::cout);
+        }
         else if(cmdline.isset("waveform"))
         {
           message.status() << "Counterexample:" << messaget::eom;

src/trans-netlist/trans_trace.cpp

@@ -811,3 +811,65 @@ void show_trans_trace_vcd(
     show_trans_state_vcd(t, trace.states[t-1], trace.states[t], ns, out);
 }
 
+/*******************************************************************\
+
+Function: show_trans_state_numbered
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_trans_state_numbered(
+  std::size_t timeframe,
+  const trans_tracet::statet &state,
+  const namespacet &ns)
+{
+  for(const auto &a : state.assignments)
+  {
+    DATA_INVARIANT(
+      a.lhs.id() == ID_symbol, "trace assignment lhs must be symbol");
+
+    const symbolt &symbol = ns.lookup(to_symbol_expr(a.lhs));
+
+    std::cout << symbol.display_name() << '@' << timeframe << " = ";
+
+    const exprt &rhs = a.rhs;
+
+    if(rhs.is_nil())
+      std::cout << "?";
+    else
+      std::cout << from_expr(ns, symbol.name, rhs);
+
+    std::cout << '\n';
+  }
+}
+
+/*******************************************************************\
+
+Function: show_trans_trace_numbered
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_trans_trace_numbered(
+  const trans_tracet &trace,
+  messaget &message,
+  const namespacet &ns,
+  std::ostream &out)
+{
+  PRECONDITION(!trace.states.empty());
+
+  auto l = trace.get_min_failing_timeframe().value_or(trace.states.size() - 1);
+
+  for(std::size_t t = 0; t <= l; t++)
+    show_trans_state_numbered(t, trace.states[t], ns);
+}

src/trans-netlist/trans_trace.h

@@ -88,4 +88,10 @@ void show_trans_trace_vcd(
   const namespacet &,
   std::ostream &);
 
+void show_trans_trace_numbered(
+  const trans_tracet &,
+  messaget &,
+  const namespacet &,
+  std::ostream &);
+
 #endif