Skip to content

Commit 03b120c

Browse files
tautschnigtautschnig
authored
Merge pull request #1009 from diffblue/smv-rtctl
SMV: parsing for real-time CTL
2 parents c50315a + c95b23e commit 03b120c

File tree

7 files changed

+173
-3
lines changed

7 files changed

+173
-3
lines changed

‎regression/smv/CTL/rtctlspec1.smv

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
MODULE main
2+
3+
-- error, this is RT-CTL
4+
SPEC EBF 1..2 FALSE

‎src/hw_cbmc_irep_ids.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,12 @@ IREP_ID_ONE(smv_S)
3131
IREP_ID_ONE(smv_T)
3232
IREP_ID_ONE(smv_Y)
3333
IREP_ID_ONE(smv_Z)
34+
IREP_ID_ONE(smv_EBF)
35+
IREP_ID_ONE(smv_ABF)
36+
IREP_ID_ONE(smv_EBG)
37+
IREP_ID_ONE(smv_ABG)
38+
IREP_ID_ONE(smv_ABU)
39+
IREP_ID_ONE(smv_EBU)
3440
IREP_ID_ONE(sva_accept_on)
3541
IREP_ID_ONE(sva_reject_on)
3642
IREP_ID_ONE(sva_sync_accept_on)

‎src/smvlang/expr2smv.cpp

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,19 @@ class expr2smvt
7575
const std::string &symbol,
7676
precedencet precedence);
7777

78+
bool convert_rtctl(
79+
const ternary_exprt &src,
80+
std::string &dest,
81+
const std::string &symbol,
82+
precedencet precedence);
83+
84+
bool convert_rtctl(
85+
const multi_ary_exprt &src,
86+
std::string &dest,
87+
const std::string &symbol1,
88+
const std::string &symbol2,
89+
precedencet precedence);
90+
7891
bool convert_unary(
7992
const unary_exprt &,
8093
std::string &dest,
@@ -240,6 +253,61 @@ bool expr2smvt::convert_binary(
240253

241254
/*******************************************************************\
242255
256+
Function: expr2smvt::convert_rtctl
257+
258+
Inputs:
259+
260+
Outputs:
261+
262+
Purpose:
263+
264+
\*******************************************************************/
265+
266+
bool expr2smvt::convert_rtctl(
267+
const ternary_exprt &src,
268+
std::string &dest,
269+
const std::string &symbol,
270+
precedencet precedence)
271+
{
272+
std::string op0, op1, op2;
273+
convert(src.op0(), op0);
274+
convert(src.op1(), op1);
275+
convert(src.op2(), op2);
276+
dest = symbol + ' ' + op0 + ".." + op1 + ' ' + op2;
277+
return false;
278+
}
279+
280+
/*******************************************************************\
281+
282+
Function: expr2smvt::convert_rtctl
283+
284+
Inputs:
285+
286+
Outputs:
287+
288+
Purpose:
289+
290+
\*******************************************************************/
291+
292+
bool expr2smvt::convert_rtctl(
293+
const multi_ary_exprt &src,
294+
std::string &dest,
295+
const std::string &symbol1,
296+
const std::string &symbol2,
297+
precedencet precedence)
298+
{
299+
std::string op0, op1, op2, op3;
300+
convert(src.op0(), op0);
301+
convert(src.op1(), op1);
302+
convert(src.op2(), op2);
303+
convert(src.op3(), op3);
304+
dest = symbol1 + '[' + op0 + ' ' + symbol2 + ' ' + op1 + ".." + op2 + ' ' +
305+
op3 + ']';
306+
return false;
307+
}
308+
309+
/*******************************************************************\
310+
243311
Function: expr2smvt::convert_unary
244312
245313
Inputs:
@@ -601,6 +669,27 @@ bool expr2smvt::convert(
601669
precedence = precedencet::TEMPORAL);
602670
}
603671

672+
else if(
673+
src.id() == ID_smv_EBF || src.id() == ID_smv_ABF ||
674+
src.id() == ID_smv_EBG || src.id() == ID_smv_ABG)
675+
{
676+
return convert_rtctl(
677+
to_ternary_expr(src),
678+
dest,
679+
std::string(src.id_string(), 4, std::string::npos),
680+
precedence = precedencet::TEMPORAL);
681+
}
682+
683+
else if(src.id() == ID_smv_EBU || src.id() == ID_smv_ABU)
684+
{
685+
return convert_rtctl(
686+
to_multi_ary_expr(src),
687+
dest,
688+
std::string(src.id_string(), 4, 1),
689+
std::string(src.id_string(), 5, std::string::npos),
690+
precedence = precedencet::TEMPORAL);
691+
}
692+
604693
else if(src.id() == ID_R)
605694
{
606695
// LTL release is "V" in NuSMV

‎src/smvlang/parser.y

Lines changed: 29 additions & 2 deletions
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 H_Token O_Token S_Token T_Token X_Token Y_Token Z_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 EBF_Token ABF_Token EBG_Token ABG_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
@@ -714,12 +714,39 @@ term : variable_name
714714
| O_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
715715
| term S_Token term { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
716716
| term T_Token term { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
717+
/* Real-time CTL */
718+
| EBF_Token range term { $$ = $1; stack_expr($$).id(ID_smv_EBF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
719+
| ABF_Token range term { $$ = $1; stack_expr($$).id(ID_smv_ABF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
720+
| EBG_Token range term { $$ = $1; stack_expr($$).id(ID_smv_EBG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
721+
| ABG_Token range term { $$ = $1; stack_expr($$).id(ID_smv_ABG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
722+
| A_Token '[' term BU_Token range term ']'
723+
{
724+
$$ = $1;
725+
stack_expr($$).id(ID_smv_ABU);
726+
mto($$, $3);
727+
stack_expr($$).add_to_operands(stack_expr($5).operands()[0]);
728+
stack_expr($$).add_to_operands(stack_expr($5).operands()[1]);
729+
mto($$, $6);
730+
}
731+
| E_Token '[' term BU_Token range term ']'
732+
{
733+
$$ = $1;
734+
stack_expr($$).id(ID_smv_EBU);
735+
mto($$, $3);
736+
stack_expr($$).add_to_operands(stack_expr($5).operands()[0]);
737+
stack_expr($$).add_to_operands(stack_expr($5).operands()[1]);
738+
mto($$, $6);
739+
}
717740
;
718741

719-
bound: '[' NUMBER_Token ',' NUMBER_Token ']'
742+
bound : '[' NUMBER_Token ',' NUMBER_Token ']'
720743
{ init($$); mto($$, $2); mto($$, $4); }
721744
;
722745

746+
range : NUMBER_Token DOTDOT_Token NUMBER_Token
747+
{ init($$); mto($$, $1); mto($$, $3); }
748+
;
749+
723750
formula_list:
724751
formula { init($$); mto($$, $1); }
725752
| formula_list ',' formula { $$=$1; mto($$, $3); }

‎src/smvlang/smv_typecheck.cpp

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -986,6 +986,31 @@ void smv_typecheckt::typecheck_expr_rec(
986986
typecheck_expr_rec(op, mode);
987987
convert_expr_to(op, expr.type());
988988
}
989+
else if(
990+
expr.id() == ID_smv_EBF || expr.id() == ID_smv_ABF ||
991+
expr.id() == ID_smv_EBG || expr.id() == ID_smv_ABG)
992+
{
993+
if(mode != CTL)
994+
throw errort().with_location(expr.source_location())
995+
<< "CTL operator not permitted here";
996+
expr.type() = bool_typet();
997+
auto &op2 = to_ternary_expr(expr).op2();
998+
typecheck_expr_rec(op2, mode);
999+
convert_expr_to(op2, expr.type());
1000+
}
1001+
else if(expr.id() == ID_smv_ABU || expr.id() == ID_smv_EBU)
1002+
{
1003+
if(mode != CTL)
1004+
throw errort().with_location(expr.source_location())
1005+
<< "CTL operator not permitted here";
1006+
expr.type() = bool_typet();
1007+
for(std::size_t i = 0; i < expr.operands().size(); i++)
1008+
{
1009+
typecheck_expr_rec(expr.operands()[i], mode);
1010+
if(i == 0 || i == 3)
1011+
convert_expr_to(expr.operands()[i], expr.type());
1012+
}
1013+
}
9891014
else if(
9901015
expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G ||
9911016
expr.id() == ID_smv_H || expr.id() == ID_smv_O || expr.id() == ID_smv_Y ||

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ bool is_temporal_operator(const exprt &expr)
1414
{
1515
return is_CTL_operator(expr) || is_LTL_operator(expr) ||
1616
is_LTL_past_operator(expr) || is_SVA_operator(expr) ||
17-
expr.id() == ID_A || expr.id() == ID_E;
17+
is_RTCTL_operator(expr) || expr.id() == ID_A || expr.id() == ID_E;
1818
}
1919

2020
bool has_temporal_operator(const exprt &expr)
@@ -27,6 +27,18 @@ bool is_exists_path(const exprt &expr)
2727
return expr.id() == ID_sva_cover;
2828
}
2929

30+
bool is_RTCTL_operator(const exprt &expr)
31+
{
32+
auto id = expr.id();
33+
return id == ID_smv_EBF || id == ID_smv_ABF || id == ID_smv_EBG ||
34+
id == ID_smv_ABG || id == ID_smv_ABU || id == ID_smv_EBU;
35+
}
36+
37+
bool has_RTCTL_operator(const exprt &expr)
38+
{
39+
return has_subexpr(expr, is_RTCTL_operator);
40+
}
41+
3042
bool is_CTL_operator(const exprt &expr)
3143
{
3244
auto id = expr.id();

‎src/temporal-logic/temporal_logic.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,13 @@ bool is_CTL_operator(const exprt &);
3232
/// Returns true iff the given expression contains a CTL operator
3333
bool has_CTL_operator(const exprt &);
3434

35+
/// Returns true iff the given expression has a real-time CTL operator
36+
/// as its root
37+
bool is_RTCTL_operator(const exprt &);
38+
39+
/// Returns true iff the given expression contains a real-time CTL operator
40+
bool has_RTCTL_operator(const exprt &);
41+
3542
/// Returns true iff the given expression is an LTL formula
3643
bool is_LTL(const exprt &);
3744

0 commit comments

Comments
 (0)