Skip to content

Commit 76a8256

Browse files
kroeningkroening
committed
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.
1 parent b97a3e7 commit 76a8256

File tree

11 files changed

+72
-26
lines changed

11 files changed

+72
-26
lines changed

‎regression/smv/CTL/smv_ctlspec2.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
smv_ctlspec2.smv
3+
4+
^file .* line 6: next\(...\) is not allowed here$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎regression/smv/CTL/smv_ctlspec2.smv

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
MODULE main
2+
3+
VAR x : boolean;
4+
5+
-- error, next(...) is not allowed
6+
SPEC AG next(x)

‎regression/smv/CTL/smv_ctlspec3.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
smv_ctlspec3.smv
3+
4+
^file .* line 5: next\(...\) is not allowed here$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎regression/smv/CTL/smv_ctlspec3.smv

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
MODULE main
2+
3+
VAR x : boolean;
4+
5+
DEFINE y := next(x);
6+
7+
-- error, next(...) is not allowed
8+
SPEC AG y

‎regression/smv/LTL/smv_ltlspec7.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
smv_ltlspec7.smv
3+
4+
^file .* line 6: next\(...\) is not allowed here$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎regression/smv/LTL/smv_ltlspec7.smv

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
MODULE main
2+
3+
VAR x : boolean;
4+
5+
-- error, next(...) is not allowed
6+
LTLSPEC G next(x)

‎src/smvlang/smv_typecheck.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -642,6 +642,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
642642
if(expr.id()==ID_symbol ||
643643
expr.id()==ID_next_symbol)
644644
{
645+
// next_symbol is only allowed in TRANS mode
646+
if(expr.id() == ID_next_symbol && mode != TRANS && mode != OTHER)
647+
throw errort().with_location(expr.find_source_location())
648+
<< "next(...) is not allowed here";
649+
645650
const irep_idt &identifier=expr.get(ID_identifier);
646651
bool next=expr.id()==ID_next_symbol;
647652

‎src/trans-word-level/instantiate_word_level.cpp

Lines changed: 16 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -72,23 +72,22 @@ symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
7272
class wl_instantiatet
7373
{
7474
public:
75-
explicit wl_instantiatet(const mp_integer &_no_timeframes)
76-
: no_timeframes(_no_timeframes)
75+
wl_instantiatet(const mp_integer &_no_timeframes, bool _next_symbol_allowed)
76+
: no_timeframes(_no_timeframes), next_symbol_allowed(_next_symbol_allowed)
7777
{
7878
}
7979

8080
/// Instantiate the given expression for timeframe t
81-
[[nodiscard]] std::pair<mp_integer, exprt>
82-
operator()(exprt expr, const mp_integer &t) const
81+
[[nodiscard]] exprt operator()(exprt expr, const mp_integer &t) const
8382
{
8483
return instantiate_rec(std::move(expr), t);
8584
}
8685

8786
protected:
8887
const mp_integer &no_timeframes;
88+
bool next_symbol_allowed;
8989

90-
[[nodiscard]] std::pair<mp_integer, exprt>
91-
instantiate_rec(exprt, const mp_integer &t) const;
90+
[[nodiscard]] exprt instantiate_rec(exprt, const mp_integer &t) const;
9291
[[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;
9392
};
9493

@@ -104,20 +103,20 @@ Function: wl_instantiatet::instantiate_rec
104103
105104
\*******************************************************************/
106105

107-
std::pair<mp_integer, exprt>
108-
wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
106+
exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
109107
{
110108
expr.type() = instantiate_rec(expr.type(), t);
111109

112110
if(expr.id() == ID_next_symbol)
113111
{
112+
PRECONDITION(next_symbol_allowed);
114113
expr.id(ID_symbol);
115114
auto u = t + 1;
116-
return {u, timeframe_symbol(u, to_symbol_expr(std::move(expr)))};
115+
return timeframe_symbol(u, to_symbol_expr(std::move(expr)));
117116
}
118117
else if(expr.id() == ID_symbol)
119118
{
120-
return {t, timeframe_symbol(t, to_symbol_expr(std::move(expr)))};
119+
return timeframe_symbol(t, to_symbol_expr(std::move(expr)));
121120
}
122121
else if(
123122
expr.id() == ID_typecast && expr.type().id() == ID_bool &&
@@ -144,7 +143,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
144143
if(ticks > t)
145144
{
146145
// return the 'default value' for the type
147-
return {t, verilog_past.default_value()};
146+
return verilog_past.default_value();
148147
}
149148
else
150149
{
@@ -159,15 +158,12 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
159158
}
160159
else
161160
{
162-
mp_integer max = t;
163161
for(auto &op : expr.operands())
164162
{
165-
auto tmp = instantiate_rec(op, t);
166-
op = tmp.second;
167-
max = std::max(max, tmp.first);
163+
op = instantiate_rec(op, t);
168164
}
169165

170-
return {max, expr};
166+
return expr;
171167
}
172168
}
173169

@@ -205,8 +201,8 @@ exprt instantiate(
205201
const mp_integer &t,
206202
const mp_integer &no_timeframes)
207203
{
208-
wl_instantiatet wl_instantiate(no_timeframes);
209-
return wl_instantiate(expr, t).second;
204+
wl_instantiatet wl_instantiate(no_timeframes, true);
205+
return wl_instantiate(expr, t);
210206
}
211207

212208
/*******************************************************************\
@@ -221,11 +217,11 @@ Function: instantiate_property
221217
222218
\*******************************************************************/
223219

224-
std::pair<mp_integer, exprt> instantiate_property(
220+
exprt instantiate_property(
225221
const exprt &expr,
226222
const mp_integer &current,
227223
const mp_integer &no_timeframes)
228224
{
229-
wl_instantiatet wl_instantiate(no_timeframes);
225+
wl_instantiatet wl_instantiate(no_timeframes, false);
230226
return wl_instantiate(expr, current);
231227
}

‎src/trans-word-level/instantiate_word_level.h

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,19 +12,24 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/mp_arith.h>
1313
#include <util/std_expr.h>
1414

15+
// Instantiate a expression in the given time frame.
16+
// May contain next_symbol, but must not contain any temporal operators.
1517
exprt instantiate(
1618
const exprt &expr,
1719
const mp_integer &current,
1820
const mp_integer &no_timeframes);
1921

20-
std::pair<mp_integer, exprt> instantiate_property(
22+
// Instantiate an atomic state predicate in the given time frame.
23+
// Must not contain next_symbol or any temporal operators.
24+
exprt instantiate_property(
2125
const exprt &,
2226
const mp_integer &current,
2327
const mp_integer &no_timeframes);
2428

2529
std::string
2630
timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);
2731

32+
// Instantiate a symbol in the given time frame.
2833
symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt);
2934

3035
#endif

‎src/trans-word-level/property.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -517,8 +517,7 @@ static obligationst property_obligations_rec(
517517
{
518518
// we rely on NNF
519519
auto &if_expr = to_if_expr(property_expr);
520-
auto cond =
521-
instantiate_property(if_expr.cond(), current, no_timeframes).second;
520+
auto cond = instantiate_property(if_expr.cond(), current, no_timeframes);
522521
auto obligations_true =
523522
property_obligations_rec(if_expr.true_case(), current, no_timeframes)
524523
.conjunction();
@@ -577,7 +576,7 @@ static obligationst property_obligations_rec(
577576
{
578577
// state formula
579578
return obligationst{
580-
instantiate_property(property_expr, current, no_timeframes)};
579+
current, instantiate_property(property_expr, current, no_timeframes)};
581580
}
582581
}
583582
else if(property_expr.id() == ID_sva_implies)
@@ -721,7 +720,7 @@ static obligationst property_obligations_rec(
721720
else
722721
{
723722
return obligationst{
724-
instantiate_property(property_expr, current, no_timeframes)};
723+
current, instantiate_property(property_expr, current, no_timeframes)};
725724
}
726725
}
727726

‎src/trans-word-level/sequence.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -456,7 +456,7 @@ sequence_matchest instantiate_sequence(
456456
// a state predicate
457457
auto &predicate = to_sva_boolean_expr(expr).op();
458458
auto instantiated = instantiate_property(predicate, t, no_timeframes);
459-
return {{instantiated.first, instantiated.second}};
459+
return {{t, instantiated}};
460460
}
461461
else
462462
{

0 commit comments

Comments
 (0)