Skip to content

Commit 2ae3ac7

Browse files
tautschnigtautschnig
authored
Merge pull request #1007 from diffblue/smv-ltl-past
SMV: past LTL operators
2 parents cbe50c6 + 72803e5 commit 2ae3ac7

File tree

8 files changed

+105
-4
lines changed

8 files changed

+105
-4
lines changed

‎regression/smv/LTL/smv_ltlspec_H1.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
smv_ltlspec_H1.smv
3+
--bound 2
4+
^\[spec1\] H x != 5: FAILURE: property not supported by BMC engine$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/smv/LTL/smv_ltlspec_H1.smv‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
MODULE main
2+
3+
VAR x : 0..10;
4+
5+
ASSIGN
6+
init(x) := 1;
7+
8+
next(x) :=
9+
case
10+
x>=3 : 3;
11+
TRUE: x+1;
12+
esac;
13+
14+
LTLSPEC H x != 5

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,14 @@ IREP_ID_TWO(C_smv_iff, "#smv_iff")
2323
IREP_ID_ONE(smv_setin)
2424
IREP_ID_ONE(smv_setnotin)
2525
IREP_ID_ONE(smv_union)
26+
IREP_ID_ONE(smv_H)
27+
IREP_ID_ONE(smv_bounded_H)
28+
IREP_ID_ONE(smv_O)
29+
IREP_ID_ONE(smv_bounded_O)
30+
IREP_ID_ONE(smv_S)
31+
IREP_ID_ONE(smv_T)
32+
IREP_ID_ONE(smv_Y)
33+
IREP_ID_ONE(smv_Z)
2634
IREP_ID_ONE(sva_accept_on)
2735
IREP_ID_ONE(sva_reject_on)
2836
IREP_ID_ONE(sva_sync_accept_on)

‎src/smvlang/expr2smv.cpp‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -564,6 +564,26 @@ bool expr2smvt::convert(
564564
precedence = precedencet::TEMPORAL);
565565
}
566566

567+
else if(
568+
src.id() == ID_smv_H || src.id() == ID_smv_O || src.id() == ID_smv_Y ||
569+
src.id() == ID_smv_Z)
570+
{
571+
return convert_unary(
572+
to_unary_expr(src),
573+
dest,
574+
std::string(src.id_string(), 4, std::string::npos) + " ",
575+
precedence = precedencet::TEMPORAL);
576+
}
577+
578+
else if(src.id() == ID_smv_bounded_H || src.id() == ID_smv_bounded_O)
579+
{
580+
return convert_unary(
581+
to_unary_expr(src),
582+
dest,
583+
std::string(src.id_string(), 12, std::string::npos) + " ",
584+
precedence = precedencet::TEMPORAL);
585+
}
586+
567587
else if(
568588
src.id() == ID_AU || src.id() == ID_EU || src.id() == ID_AR ||
569589
src.id() == ID_ER || src.id() == ID_U)
@@ -582,6 +602,15 @@ bool expr2smvt::convert(
582602
to_binary_expr(src), dest, "V", precedence = precedencet::TEMPORAL);
583603
}
584604

605+
else if(src.id() == ID_smv_S || src.id() == ID_smv_T)
606+
{
607+
return convert_binary(
608+
to_binary_expr(src),
609+
dest,
610+
std::string(src.id_string(), 4, std::string::npos),
611+
precedence = precedencet::TEMPORAL);
612+
}
613+
585614
else if(src.id() == ID_if)
586615
return convert_if(to_if_expr(src), dest, precedencet::IF);
587616

‎src/smvlang/parser.y‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,7 @@ static void new_module(YYSTYPE &module)
284284
%left OR_Token
285285
%left AND_Token
286286
%left NOT_Token
287-
%left EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token X_Token
287+
%left EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token H_Token O_Token S_Token T_Token X_Token Y_Token Z_Token
288288
%left EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
289289
%left union_Token
290290
%left IN_Token NOTIN_Token
@@ -704,6 +704,19 @@ term : variable_name
704704
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
705705
| term IN_Token term { binary($$, $1, ID_smv_setin, $3); }
706706
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); }
707+
/* LTL PAST */
708+
| Y_Token term { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); }
709+
| Z_Token term { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); }
710+
| H_Token term { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); }
711+
| H_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); }
712+
| O_Token term { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); }
713+
| O_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
714+
| term S_Token term { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
715+
| term T_Token term { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
716+
;
717+
718+
bound: '[' NUMBER_Token ',' NUMBER_Token ']'
719+
{ init($$); mto($$, $2); mto($$, $4); }
707720
;
708721

709722
formula_list:

‎src/smvlang/smv_typecheck.cpp‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -986,7 +986,10 @@ void smv_typecheckt::typecheck_expr_rec(
986986
typecheck_expr_rec(op, mode);
987987
convert_expr_to(op, expr.type());
988988
}
989-
else if(expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G)
989+
else if(
990+
expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G ||
991+
expr.id() == ID_smv_H || expr.id() == ID_smv_O || expr.id() == ID_smv_Y ||
992+
expr.id() == ID_smv_Z)
990993
{
991994
if(mode != LTL)
992995
throw errort().with_location(expr.source_location())
@@ -1010,7 +1013,9 @@ void smv_typecheckt::typecheck_expr_rec(
10101013
convert_expr_to(binary_expr.lhs(), expr.type());
10111014
convert_expr_to(binary_expr.rhs(), expr.type());
10121015
}
1013-
else if(expr.id() == ID_U || expr.id() == ID_R)
1016+
else if(
1017+
expr.id() == ID_U || expr.id() == ID_R || expr.id() == ID_smv_S ||
1018+
expr.id() == ID_smv_T)
10141019
{
10151020
if(mode != LTL)
10161021
throw errort().with_location(expr.source_location())

‎src/temporal-logic/temporal_logic.cpp‎

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
1313
bool is_temporal_operator(const exprt &expr)
1414
{
1515
return is_CTL_operator(expr) || is_LTL_operator(expr) ||
16-
is_SVA_operator(expr) || expr.id() == ID_A || expr.id() == ID_E;
16+
is_LTL_past_operator(expr) || is_SVA_operator(expr) ||
17+
expr.id() == ID_A || expr.id() == ID_E;
1718
}
1819

1920
bool has_temporal_operator(const exprt &expr)
@@ -54,6 +55,14 @@ bool is_LTL_operator(const exprt &expr)
5455
return id == ID_G || id == ID_F || id == ID_X || id == ID_U || id == ID_R;
5556
}
5657

58+
bool is_LTL_past_operator(const exprt &expr)
59+
{
60+
auto id = expr.id();
61+
return id == ID_smv_H || id == ID_smv_bounded_H || id == ID_smv_O ||
62+
id == ID_smv_bounded_O || id == ID_smv_S || id == ID_smv_T ||
63+
id == ID_smv_Y || id == ID_smv_Z;
64+
}
65+
5766
bool is_LTL(const exprt &expr)
5867
{
5968
auto non_LTL_operator = [](const exprt &expr) {
@@ -63,6 +72,14 @@ bool is_LTL(const exprt &expr)
6372
return !has_subexpr(expr, non_LTL_operator);
6473
}
6574

75+
bool is_LTL_past(const exprt &expr)
76+
{
77+
auto non_LTL_past_operator = [](const exprt &expr)
78+
{ return is_temporal_operator(expr) && !is_LTL_past_operator(expr); };
79+
80+
return !has_subexpr(expr, non_LTL_past_operator);
81+
}
82+
6683
bool is_SVA_sequence(const exprt &expr)
6784
{
6885
auto id = expr.id();

‎src/temporal-logic/temporal_logic.h‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,10 +35,17 @@ bool has_CTL_operator(const exprt &);
3535
/// Returns true iff the given expression is an LTL formula
3636
bool is_LTL(const exprt &);
3737

38+
/// Returns true iff the given expression is an LTL past formula
39+
bool is_LTL_past(const exprt &);
40+
3841
/// Returns true iff the given expression has an LTL operator
3942
/// as its root
4043
bool is_LTL_operator(const exprt &);
4144

45+
/// Returns true iff the given expression has an LTL past operator
46+
/// as its root
47+
bool is_LTL_past_operator(const exprt &);
48+
4249
/// Returns true iff the given expression is an SVA sequence expression
4350
bool is_SVA_sequence(const exprt &);
4451

0 commit comments

Comments
 (0)