Skip to content

SMV: past LTL operators #1007

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 24, 2025
Merged

SMV: past LTL operators #1007

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions regression/smv/LTL/smv_ltlspec_H1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
smv_ltlspec_H1.smv
--bound 2
^\[spec1\] H x != 5: FAILURE: property not supported by BMC engine$
^EXIT=10$
^SIGNAL=0$
--
^warning: ignoring
14 changes: 14 additions & 0 deletions regression/smv/LTL/smv_ltlspec_H1.smv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
MODULE main

VAR x : 0..10;

ASSIGN
init(x) := 1;

next(x) :=
case
x>=3 : 3;
TRUE: x+1;
esac;

LTLSPEC H x != 5
8 changes: 8 additions & 0 deletions src/hw_cbmc_irep_ids.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,14 @@ IREP_ID_TWO(C_smv_iff, "#smv_iff")
IREP_ID_ONE(smv_setin)
IREP_ID_ONE(smv_setnotin)
IREP_ID_ONE(smv_union)
IREP_ID_ONE(smv_H)
IREP_ID_ONE(smv_bounded_H)
IREP_ID_ONE(smv_O)
IREP_ID_ONE(smv_bounded_O)
IREP_ID_ONE(smv_S)
IREP_ID_ONE(smv_T)
IREP_ID_ONE(smv_Y)
IREP_ID_ONE(smv_Z)
IREP_ID_ONE(sva_accept_on)
IREP_ID_ONE(sva_reject_on)
IREP_ID_ONE(sva_sync_accept_on)
Expand Down
29 changes: 29 additions & 0 deletions src/smvlang/expr2smv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -564,6 +564,26 @@ bool expr2smvt::convert(
precedence = precedencet::TEMPORAL);
}

else if(
src.id() == ID_smv_H || src.id() == ID_smv_O || src.id() == ID_smv_Y ||
src.id() == ID_smv_Z)
{
return convert_unary(
to_unary_expr(src),
dest,
std::string(src.id_string(), 4, std::string::npos) + " ",
precedence = precedencet::TEMPORAL);
}

else if(src.id() == ID_smv_bounded_H || src.id() == ID_smv_bounded_O)
{
return convert_unary(
to_unary_expr(src),
dest,
std::string(src.id_string(), 12, std::string::npos) + " ",
precedence = precedencet::TEMPORAL);
}

else if(
src.id() == ID_AU || src.id() == ID_EU || src.id() == ID_AR ||
src.id() == ID_ER || src.id() == ID_U)
Expand All @@ -582,6 +602,15 @@ bool expr2smvt::convert(
to_binary_expr(src), dest, "V", precedence = precedencet::TEMPORAL);
}

else if(src.id() == ID_smv_S || src.id() == ID_smv_T)
{
return convert_binary(
to_binary_expr(src),
dest,
std::string(src.id_string(), 4, std::string::npos),
precedence = precedencet::TEMPORAL);
}

else if(src.id() == ID_if)
return convert_if(to_if_expr(src), dest, precedencet::IF);

Expand Down
15 changes: 14 additions & 1 deletion src/smvlang/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ static void new_module(YYSTYPE &module)
%left OR_Token
%left AND_Token
%left NOT_Token
%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
%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
%left EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
%left union_Token
%left IN_Token NOTIN_Token
Expand Down Expand Up @@ -704,6 +704,19 @@ term : variable_name
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
| term IN_Token term { binary($$, $1, ID_smv_setin, $3); }
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); }
/* LTL PAST */
| Y_Token term { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); }
| Z_Token term { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); }
| H_Token term { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); }
| H_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); }
| O_Token term { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); }
| O_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
| term S_Token term { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
| term T_Token term { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
;

bound: '[' NUMBER_Token ',' NUMBER_Token ']'
{ init($$); mto($$, $2); mto($$, $4); }
;

formula_list:
Expand Down
9 changes: 7 additions & 2 deletions src/smvlang/smv_typecheck.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -986,7 +986,10 @@ void smv_typecheckt::typecheck_expr_rec(
typecheck_expr_rec(op, mode);
convert_expr_to(op, expr.type());
}
else if(expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G)
else if(
expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G ||
expr.id() == ID_smv_H || expr.id() == ID_smv_O || expr.id() == ID_smv_Y ||
expr.id() == ID_smv_Z)
{
if(mode != LTL)
throw errort().with_location(expr.source_location())
Expand All @@ -1010,7 +1013,9 @@ void smv_typecheckt::typecheck_expr_rec(
convert_expr_to(binary_expr.lhs(), expr.type());
convert_expr_to(binary_expr.rhs(), expr.type());
}
else if(expr.id() == ID_U || expr.id() == ID_R)
else if(
expr.id() == ID_U || expr.id() == ID_R || expr.id() == ID_smv_S ||
expr.id() == ID_smv_T)
{
if(mode != LTL)
throw errort().with_location(expr.source_location())
Expand Down
19 changes: 18 additions & 1 deletion src/temporal-logic/temporal_logic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ Author: Daniel Kroening, [email protected]
bool is_temporal_operator(const exprt &expr)
{
return is_CTL_operator(expr) || is_LTL_operator(expr) ||
is_SVA_operator(expr) || expr.id() == ID_A || expr.id() == ID_E;
is_LTL_past_operator(expr) || is_SVA_operator(expr) ||
expr.id() == ID_A || expr.id() == ID_E;
}

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

bool is_LTL_past_operator(const exprt &expr)
{
auto id = expr.id();
return id == ID_smv_H || id == ID_smv_bounded_H || id == ID_smv_O ||
id == ID_smv_bounded_O || id == ID_smv_S || id == ID_smv_T ||
id == ID_smv_Y || id == ID_smv_Z;
}

bool is_LTL(const exprt &expr)
{
auto non_LTL_operator = [](const exprt &expr) {
Expand All @@ -63,6 +72,14 @@ bool is_LTL(const exprt &expr)
return !has_subexpr(expr, non_LTL_operator);
}

bool is_LTL_past(const exprt &expr)
{
auto non_LTL_past_operator = [](const exprt &expr)
{ return is_temporal_operator(expr) && !is_LTL_past_operator(expr); };

return !has_subexpr(expr, non_LTL_past_operator);
Comment on lines +75 to +80
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is that implemented via negation? This makes is_LTL_PAST(nil_exprt{}) return true?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that's desired -- say "true" is CTL, LTL, LTL+past, CTL*, etc.

}

bool is_SVA_sequence(const exprt &expr)
{
auto id = expr.id();
Expand Down
7 changes: 7 additions & 0 deletions src/temporal-logic/temporal_logic.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,17 @@ bool has_CTL_operator(const exprt &);
/// Returns true iff the given expression is an LTL formula
bool is_LTL(const exprt &);

/// Returns true iff the given expression is an LTL past formula
bool is_LTL_past(const exprt &);

/// Returns true iff the given expression has an LTL operator
/// as its root
bool is_LTL_operator(const exprt &);

/// Returns true iff the given expression has an LTL past operator
/// as its root
bool is_LTL_past_operator(const exprt &);

/// Returns true iff the given expression is an SVA sequence expression
bool is_SVA_sequence(const exprt &);

Expand Down
Loading