SMV: named properties

NuSMV allows naming properties.

Author: kroening

regression/smv/LTL/smv_ltlspec4.desc

@@ -3,12 +3,12 @@ smv_ltlspec4.smv
 --bound 10 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[spec1\] F x = 0: REFUTED$
+^\[p1\] F x = 0: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
 ^x@1 = 2$
 ^x@2 = 2$
-^\[spec2\] F x = 2: PROVED up to bound 10$
+^\[p2\] F x = 2: PROVED up to bound 10$
 --
 ^warning: ignoring
 --

regression/smv/LTL/smv_ltlspec4.smv

@@ -6,5 +6,5 @@ ASSIGN
   init(x) := 1;
   next(x) := 2;
 
-LTLSPEC F x=0 -- fails
-LTLSPEC F x=2 -- holds
+LTLSPEC NAME p1 := F x=0 -- fails
+LTLSPEC NAME p2 := F x=2 -- holds

regression/smv/range-type/range_type1.desc

@@ -3,6 +3,6 @@ range_type1.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[spec1\] AG x != 4: PROVED up to bound 10$
+^\[p1\] AG x != 4: PROVED up to bound 10$
 --
 ^warning: ignoring

regression/smv/range-type/range_type1.smv

@@ -19,4 +19,4 @@ ASSIGN
       TRUE: 4;
     esac;
 
-SPEC AG x!=4
+SPEC NAME p1 := AG x!=4

src/smvlang/parser.y

@@ -372,13 +372,49 @@ fairness_constraint:
            ;
 
 ctl_specification:
-             SPEC_Token formula semi_opt { PARSER.module->add_ctlspec(stack_expr($2), stack_expr($1).source_location()); }
+             SPEC_Token formula semi_opt
+           {
+             PARSER.module->add_ctlspec(
+               stack_expr($2),
+               stack_expr($1).source_location());
+           }
            | SPEC_Token
+           | CTLSPEC_Token formula semi_opt
+           {
+             PARSER.module->add_ctlspec(
+               stack_expr($2),
+               stack_expr($1).source_location());
+           }
+           | CTLSPEC_Token
+           | SPEC_Token NAME_Token identifier BECOMES_Token formula semi_opt
+           {
+             PARSER.module->add_ctlspec(
+               stack_expr($3).id(),
+               stack_expr($5),
+               stack_expr($1).source_location());
+           }
+           | CTLSPEC_Token NAME_Token identifier BECOMES_Token formula semi_opt
+           {
+             PARSER.module->add_ctlspec(
+               stack_expr($3).id(),
+               stack_expr($5),
+               stack_expr($1).source_location());
+           }
            ;
 
 ltl_specification:
-             LTLSPEC_Token formula semi_opt { PARSER.module->add_ltlspec(stack_expr($2), stack_expr($1).source_location()); }
-           | LTLSPEC_Token
+             LTLSPEC_Token formula semi_opt
+           { 
+             PARSER.module->add_ltlspec(stack_expr($2), stack_expr($1).source_location());
+           }
+           | LTLSPEC_Token           
+           | LTLSPEC_Token NAME_Token identifier BECOMES_Token formula semi_opt
+           { 
+             PARSER.module->add_ltlspec(
+               stack_expr($3).id(),
+               stack_expr($5),
+               stack_expr($1).source_location());
+           }
            ;
 
 extern_var : variable_name EQUAL_Token QUOTE_Token
@@ -669,9 +705,13 @@ term       : variable_name
            | term NOTIN_Token    term { binary($$, $1, ID_smv_setnotin, $3); }
            ;
 
-formula_list: formula { init($$); mto($$, $1); }
-            | formula_list ',' formula { $$=$1; mto($$, $3); }
-            ;
+formula_list:
+             formula { init($$); mto($$, $1); }
+           | formula_list ',' formula { $$=$1; mto($$, $3); }
+           ;
+
+identifier : STRING_Token
+           ;
 
 variable_name: qstring_list
            {

src/smvlang/smv_parse_tree.h

@@ -61,9 +61,22 @@ class smv_parse_treet
       {
       }
 
+      itemt(
+        item_typet __item_type,
+        irep_idt __name,
+        exprt __expr,
+        source_locationt __location)
+        : item_type(__item_type),
+          name(__name),
+          expr(std::move(__expr)),
+          location(std::move(__location))
+      {
+      }
+
       friend std::string to_string(item_typet i);
 
       item_typet item_type;
+      std::optional<irep_idt> name;
       exprt expr;
       source_locationt location;
 
@@ -163,18 +176,6 @@ class smv_parse_treet
         itemt::INVAR, std::move(expr), source_locationt::nil());
     }
 
-    void add_ctlspec(exprt expr)
-    {
-      items.emplace_back(
-        itemt::CTLSPEC, std::move(expr), source_locationt::nil());
-    }
-
-    void add_ltlspec(exprt expr)
-    {
-      items.emplace_back(
-        itemt::LTLSPEC, std::move(expr), source_locationt::nil());
-    }
-
     void add_define(exprt lhs, exprt rhs)
     {
       items.emplace_back(
@@ -210,11 +211,22 @@ class smv_parse_treet
       items.emplace_back(itemt::CTLSPEC, std::move(expr), std::move(location));
     }
 
+    void add_ctlspec(irep_idt name, exprt expr, source_locationt location)
+    {
+      items.emplace_back(
+        itemt::CTLSPEC, name, std::move(expr), std::move(location));
+    }
+
     void add_ltlspec(exprt expr, source_locationt location)
     {
       items.emplace_back(itemt::LTLSPEC, std::move(expr), location);
     }
 
+    void add_ltlspec(irep_idt name, exprt expr, source_locationt location)
+    {
+      items.emplace_back(itemt::LTLSPEC, name, std::move(expr), location);
+    }
+
     void add_define(exprt expr, source_locationt location)
     {
       items.emplace_back(itemt::DEFINE, std::move(expr), std::move(location));

src/smvlang/smv_typecheck.cpp

@@ -1590,7 +1590,11 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
       {
         symbolt spec_symbol;
 
-        spec_symbol.base_name = "spec" + std::to_string(nr++);
+        if(it->name.has_value())
+          spec_symbol.base_name = it->name.value();
+        else
+          spec_symbol.base_name = "spec" + std::to_string(nr++);
+
         spec_symbol.name =
           id2string(smv_module.name) + "::" + id2string(spec_symbol.base_name);
         spec_symbol.module = smv_module.name;