SMV: properties must not contain next(...)

This adds a check to the SMV type checker that prohibits the use of
next(...) inside temporal-logic properties.  This matches the behavior of
NuSMV.

Author: kroening

regression/smv/CTL/smv_ctlspec2.desc

@@ -0,0 +1,7 @@
+CORE
+smv_ctlspec2.smv
+
+^file .* line 6: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/smv/CTL/smv_ctlspec2.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- error, next(...) is not allowed
+SPEC AG next(x)

regression/smv/LTL/smv_ltlspec7.desc

@@ -0,0 +1,7 @@
+CORE
+smv_ltlspec7.smv
+
+^file .* line 6: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/smv/LTL/smv_ltlspec7.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- error, next(...) is not allowed
+LTLSPEC G next(x)

src/smvlang/smv_typecheck.cpp

@@ -642,6 +642,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   if(expr.id()==ID_symbol || 
      expr.id()==ID_next_symbol)
   {
+    // next_symbol is only allowed in TRANS mode
+    if(expr.id() == ID_next_symbol && mode != TRANS)
+      throw errort().with_location(expr.find_source_location())
+        << "next(...) is not allowed here";
+
     const irep_idt &identifier=expr.get(ID_identifier);
     bool next=expr.id()==ID_next_symbol;
 

src/trans-word-level/instantiate_word_level.cpp

@@ -72,8 +72,8 @@ symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
 class wl_instantiatet
 {
 public:
-  explicit wl_instantiatet(const mp_integer &_no_timeframes)
-    : no_timeframes(_no_timeframes)
+  wl_instantiatet(const mp_integer &_no_timeframes, bool _next_symbol_allowed)
+    : no_timeframes(_no_timeframes), next_symbol_allowed(_next_symbol_allowed)
   {
   }
 
@@ -86,6 +86,7 @@ class wl_instantiatet
 
 protected:
   const mp_integer &no_timeframes;
+  bool next_symbol_allowed;
 
   [[nodiscard]] std::pair<mp_integer, exprt>
   instantiate_rec(exprt, const mp_integer &t) const;
@@ -111,6 +112,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 
   if(expr.id() == ID_next_symbol)
   {
+    PRECONDITION(next_symbol_allowed);
     expr.id(ID_symbol);
     auto u = t + 1;
     return {u, timeframe_symbol(u, to_symbol_expr(std::move(expr)))};
@@ -205,7 +207,7 @@ exprt instantiate(
   const mp_integer &t,
   const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes);
+  wl_instantiatet wl_instantiate(no_timeframes, true);
   return wl_instantiate(expr, t).second;
 }
 
@@ -226,6 +228,6 @@ std::pair<mp_integer, exprt> instantiate_property(
   const mp_integer &current,
   const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes);
+  wl_instantiatet wl_instantiate(no_timeframes, false);
   return wl_instantiate(expr, current);
 }

src/trans-word-level/instantiate_word_level.h

@@ -12,11 +12,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/mp_arith.h>
 #include <util/std_expr.h>
 
+// Instantiate a expression in the given time frame.
+// May contain next_symbol, but must not contain any temporal operators.
 exprt instantiate(
   const exprt &expr,
   const mp_integer &current,
   const mp_integer &no_timeframes);
 
+// Instantiate an atomic state predicate in the given time frame.
+// Must not contain next_symbol or any temporal operators.
 std::pair<mp_integer, exprt> instantiate_property(
   const exprt &,
   const mp_integer &current,
@@ -25,6 +29,7 @@ std::pair<mp_integer, exprt> instantiate_property(
 std::string
 timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);
 
+// Instantiate a symbol in the given time frame.
 symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt);
 
 #endif