Merge pull request #1206 from diffblue/smv_ltlspec_F7

BMC: looping constraint must consider all inputs

Author: tautschnig

regression/ebmc/SVA-LTL/lasso1-show-formula.desc

@@ -3,6 +3,6 @@ lasso1.sv
 --bound 1 --show-formula
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) lasso::1-back-to-0 ⇔ \(.*counter@1 = .*counter@0 ∧ .*clock@1 ⇔ .*clock@0\)$
+^\(\d+\) lasso::1-back-to-0 ⇔ \(.*clock@1 ⇔ .*clock@0 ∧ .*counter@1 = .*counter@0\)$
 --
 --

regression/smv/LTL/smv_ltlspec_F5.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 smv_ltlspec_F5.smv
---bound 3 --numbered-trace
+--bound 1 --numbered-trace
 ^\[spec1\] F \(!some_input \& X !some_input\): REFUTED$
+^Counterexample with 2 states:$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The BMC engine gives the wrong answer.

regression/smv/LTL/smv_ltlspec_F5.smv

@@ -3,5 +3,5 @@ MODULE main
 VAR some_input : boolean;
 
 -- Expected to fail
--- The shortest loop is FALSE, FALSE
+-- The shortest loop is FALSE, FALSE or TRUE, TRUE
 LTLSPEC F (!some_input & X !some_input)

regression/smv/LTL/smv_ltlspec_F7.desc

@@ -0,0 +1,8 @@
+CORE
+smv_ltlspec_F7.smv
+--bound 1 --show-formula
+^\(1\) lasso::1-back-to-0 ⇔ \(smv::main::var::some_input@1 = smv::main::var::some_input@0\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/LTL/smv_ltlspec_F7.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_input : 1..3;
+
+-- Expected to fail
+LTLSPEC F (some_input >= 2)

src/trans-word-level/lasso.cpp

@@ -95,7 +95,7 @@ void lasso_constraints(
 
   std::vector<symbol_exprt> variables_to_compare;
 
-  // Gather the state variables.
+  // Gather the state variables, and the inputs.
   const symbol_tablet &symbol_table = ns.get_symbol_table();
   auto lower = symbol_table.symbol_module_map.lower_bound(module_identifier);
   auto upper = symbol_table.symbol_module_map.upper_bound(module_identifier);
@@ -104,26 +104,18 @@ void lasso_constraints(
   {
     const symbolt &symbol = ns.lookup(it->second);
 
-    if(symbol.is_state_var)
+    if(symbol.is_state_var || symbol.is_input)
       variables_to_compare.push_back(symbol.symbol_expr());
   }
 
-  // gather the top-level inputs
-  const auto &module_symbol = ns.lookup(module_identifier);
-  DATA_INVARIANT(module_symbol.type.id() == ID_module, "expected a module");
-  const auto &ports = module_symbol.type.find(ID_ports);
+  // We sort the set of variables to compare,
+  // to get a deterministic formula
+  auto ordering = [](const symbol_exprt &a, const symbol_exprt &b)
+  { return id2string(a.get_identifier()) < id2string(b.get_identifier()); };
 
-  for(auto &port : static_cast<const exprt &>(ports).operands())
-  {
-    DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
-    if(port.get_bool(ID_input) && !port.get_bool(ID_output))
-    {
-      symbol_exprt input_symbol(port.get(ID_identifier), port.type());
-      input_symbol.add_source_location() = port.source_location();
-      variables_to_compare.push_back(std::move(input_symbol));
-    }
-  }
+  std::sort(variables_to_compare.begin(), variables_to_compare.end(), ordering);
 
+  // Create the constraint
   for(mp_integer i = 1; i < no_timeframes; ++i)
   {
     for(mp_integer k = 0; k < i; ++k)