Introduce [->min..max] operator.
* src/ltlast/bunop.hh: Declare bunop::Goto * src/ltlast/bunop.cc: Handle it. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Add rules for [->min..max]. * src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Goto in the translation. * src/ltltest/equals.test: Test trivial identities. * src/tgbatest/ltl2tgba.test: Test two more formulae using [->].
This commit is contained in:
Alexandre Duret-Lutz
parent
2c31e541b5
commit
da74b4f180
7 changed files with 138 additions and 11 deletions
|
|
@ -113,6 +113,8 @@ namespace spot
|
|||
return "Equal";
|
||||
case Star:
|
||||
return "Star";
|
||||
case Goto:
|
||||
return "Goto";
|
||||
}
|
||||
// Unreachable code.
|
||||
assert(0);
|
||||
|
|
@ -124,6 +126,9 @@ namespace spot
|
|||
{
|
||||
std::ostringstream out;
|
||||
|
||||
unsigned default_min = 0;
|
||||
unsigned default_max = unbounded;
|
||||
|
||||
switch (op_)
|
||||
{
|
||||
case Star:
|
||||
|
|
@ -138,10 +143,36 @@ namespace spot
|
|||
case Equal:
|
||||
out << "[=";
|
||||
break;
|
||||
case Goto:
|
||||
out << "[->";
|
||||
default_min = 1;
|
||||
default_max = 1;
|
||||
break;
|
||||
}
|
||||
|
||||
if (min_ != 0 || max_ != unbounded)
|
||||
// Beware that the default parameters of the Goto operator are
|
||||
// not the same as Star or Equal:
|
||||
//
|
||||
// [->] = [->1..1]
|
||||
// [->..] = [->1..unbounded]
|
||||
// [*] = [*0..unbounded]
|
||||
// [*..] = [*0..unbounded]
|
||||
// [=] = [=0..unbounded]
|
||||
// [=..] = [=0..unbounded]
|
||||
//
|
||||
// Strictly speaking [=] is not specified by PSL, and anyway we
|
||||
// automatically rewrite Exp[=0..unbounded] as
|
||||
// Exp[*0..unbounded], so we should never have to print [=]
|
||||
// here.
|
||||
//
|
||||
// Also
|
||||
// [*..] = [*0..unbounded]
|
||||
|
||||
if (min_ != default_min || max_ != default_max)
|
||||
{
|
||||
// Always print the min_, even when it is equal to
|
||||
// default_min, this way we avoid ambiguities (like
|
||||
// when reading [*..3] near [*->..2])
|
||||
out << min_;
|
||||
if (min_ != max_)
|
||||
{
|
||||
|
|
@ -208,6 +239,38 @@ namespace spot
|
|||
unop::instance(unop::Not, child));
|
||||
break;
|
||||
}
|
||||
case Goto:
|
||||
{
|
||||
// - 0[->min..max] = 0 if min>0
|
||||
// - 0[->0..max] = [*0]
|
||||
if (child == constant::false_instance())
|
||||
{
|
||||
if (min == 0)
|
||||
return constant::empty_word_instance();
|
||||
else
|
||||
return child;
|
||||
}
|
||||
// - 1[->0] = [*0]
|
||||
// - 1[->min..max] = 1[*min..max]
|
||||
|
||||
if (child == constant::true_instance())
|
||||
{
|
||||
if (max == 0)
|
||||
return constant::empty_word_instance();
|
||||
else
|
||||
{
|
||||
op = Star;
|
||||
break;
|
||||
}
|
||||
}
|
||||
// - Exp[->0] = [*0]
|
||||
if (max == 0)
|
||||
{
|
||||
child->destroy();
|
||||
return constant::empty_word_instance();
|
||||
}
|
||||
break;
|
||||
}
|
||||
case Star:
|
||||
{
|
||||
// - [*0][*min..max] = [*0]
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ namespace spot
|
|||
class bunop : public ref_formula
|
||||
{
|
||||
public:
|
||||
enum type { Star, Equal };
|
||||
enum type { Star, Equal, Goto };
|
||||
|
||||
static const unsigned unbounded = -1U;
|
||||
|
||||
|
|
@ -57,6 +57,11 @@ namespace spot
|
|||
/// - 1[=min..max] = 1[*min..max] if max > 0
|
||||
/// - Exp[=0..] = [*]
|
||||
/// - Exp[=0] = (!Exp)[*]
|
||||
/// - 0[->min..max] = 0 if min>0
|
||||
/// - 0[->0..max] = [*0]
|
||||
/// - 1[->0] = [*0]
|
||||
/// - 1[->min..max] = 1[*min..max]
|
||||
/// - Exp[->0] = [*0]
|
||||
///
|
||||
/// These rewriting rules imply that it is not possible to build
|
||||
/// an LTL formula object that is SYNTACTICALLY equal to one of
|
||||
|
|
|
|||
|
|
@ -94,6 +94,7 @@ using namespace spot::ltl;
|
|||
%token OP_PLUS "plus operator"
|
||||
%token OP_STAR_OPEN "opening bracket for star operator"
|
||||
%token OP_EQUAL_OPEN "opening bracket for equal operator"
|
||||
%token OP_GOTO_OPEN "opening bracket for goto operator"
|
||||
%token OP_SQBKT_CLOSE "closing bracket"
|
||||
%token <num> OP_SQBKT_NUM "number for square bracket operator"
|
||||
%token OP_SQBKT_SEP "separator for square bracket operator"
|
||||
|
|
@ -126,7 +127,7 @@ using namespace spot::ltl;
|
|||
%nonassoc OP_X
|
||||
|
||||
/* High priority regex operator. */
|
||||
%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN
|
||||
%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN OP_GOTO_OPEN
|
||||
|
||||
/* Not has the most important priority after Wring's `=0' and `=1'. */
|
||||
%nonassoc OP_NOT
|
||||
|
|
@ -135,7 +136,7 @@ using namespace spot::ltl;
|
|||
|
||||
%type <ltl> subformula booleanatom rationalexp
|
||||
%type <ltl> bracedrationalexp parenthesedsubformula
|
||||
%type <minmax> starargs equalargs sqbracketargs
|
||||
%type <minmax> starargs equalargs sqbracketargs gotoargs
|
||||
|
||||
%destructor { delete $$; } <str>
|
||||
%destructor { $$->destroy(); } <ltl>
|
||||
|
|
@ -192,6 +193,7 @@ enderror: error END_OF_INPUT
|
|||
OP_SQBKT_SEP_opt: | OP_SQBKT_SEP
|
||||
error_opt: | error
|
||||
|
||||
/* for [*i..j] and [=i..j] */
|
||||
sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
{ $$.min = $1; $$.max = $3; }
|
||||
| OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_CLOSE
|
||||
|
|
@ -203,6 +205,28 @@ sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
|||
| OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
{ $$.min = $$.max = $1; }
|
||||
|
||||
/* [->i..j] has default values that are different than [*] and [=]. */
|
||||
gotoargs: OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
{ $$.min = $2; $$.max = $4; }
|
||||
| OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_CLOSE
|
||||
{ $$.min = $2; $$.max = bunop::unbounded; }
|
||||
| OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
{ $$.min = 1U; $$.max = $3; }
|
||||
| OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_CLOSE
|
||||
{ $$.min = 1U; $$.max = bunop::unbounded; }
|
||||
| OP_GOTO_OPEN OP_SQBKT_CLOSE
|
||||
{ $$.min = $$.max = 1U; }
|
||||
| OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
{ $$.min = $$.max = $2; }
|
||||
| OP_GOTO_OPEN error OP_SQBKT_CLOSE
|
||||
{ error_list.push_back(parse_error(@$,
|
||||
"treating this goto block as [->]"));
|
||||
$$.min = $$.max = 1U; }
|
||||
| OP_GOTO_OPEN error_opt END_OF_INPUT
|
||||
{ error_list.push_back(parse_error(@$,
|
||||
"missing closing bracket for goto operator"));
|
||||
$$.min = $$.max = 0U; }
|
||||
|
||||
starargs: OP_STAR
|
||||
{ $$.min = 0U; $$.max = bunop::unbounded; }
|
||||
| OP_PLUS
|
||||
|
|
@ -222,11 +246,11 @@ equalargs: OP_EQUAL_OPEN sqbracketargs
|
|||
{ $$ = $2; }
|
||||
| OP_EQUAL_OPEN error OP_SQBKT_CLOSE
|
||||
{ error_list.push_back(parse_error(@$,
|
||||
"treating this star block as [*]"));
|
||||
"treating this equal block as [*]"));
|
||||
$$.min = 0U; $$.max = bunop::unbounded; }
|
||||
| OP_EQUAL_OPEN error_opt END_OF_INPUT
|
||||
{ error_list.push_back(parse_error(@$,
|
||||
"missing closing bracket for star"));
|
||||
"missing closing bracket for equal operator"));
|
||||
$$.min = $$.max = 0U; }
|
||||
|
||||
|
||||
|
|
@ -352,6 +376,24 @@ rationalexp: booleanatom
|
|||
"be applied to a boolean expression"));
|
||||
error_list.push_back(parse_error(@$,
|
||||
"treating this block as false"));
|
||||
$1->destroy();
|
||||
$$ = constant::false_instance();
|
||||
}
|
||||
}
|
||||
| rationalexp gotoargs
|
||||
{
|
||||
if ((kind_of($1) & Boolean_Kind) == Boolean_Kind)
|
||||
{
|
||||
$$ = bunop::instance(bunop::Goto, $1, $2.min, $2.max);
|
||||
}
|
||||
else
|
||||
{
|
||||
error_list.push_back(parse_error(@1,
|
||||
"not a boolean expression: [->...] can only "
|
||||
"be applied to a boolean expression"));
|
||||
error_list.push_back(parse_error(@$,
|
||||
"treating this block as false"));
|
||||
$1->destroy();
|
||||
$$ = constant::false_instance();
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -98,6 +98,7 @@ flex_set_buffer(const char* buf, int start_tok)
|
|||
"[+]" BEGIN(0); return token::OP_PLUS;
|
||||
"[*" BEGIN(sqbracket); return token::OP_STAR_OPEN;
|
||||
"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
|
||||
"[->" BEGIN(sqbracket); return token::OP_GOTO_OPEN;
|
||||
<sqbracket>"]" BEGIN(0); return token::OP_SQBKT_CLOSE;
|
||||
<sqbracket>[0-9]+ {
|
||||
unsigned num = 0;
|
||||
|
|
|
|||
|
|
@ -151,3 +151,12 @@ run 0 ../equals '{1[=1..2]}' '{[*1..2]}'
|
|||
run 0 ../equals '{1[=..4]}' '{1[*..4]}'
|
||||
run 0 ../equals '{b[=0]}' '{(!b)[*]}'
|
||||
run 0 ../equals '{b[=0..]}' '{*}'
|
||||
|
||||
run 0 ../equals '{0[->10..100];b}' '0'
|
||||
run 0 ../equals '{0[->1..];b}' '0'
|
||||
run 0 ../equals '{0[->0..100];b}' '{b}'
|
||||
run 0 ../equals '{0[->0..];b}' '{b}'
|
||||
run 0 ../equals '{1[->0];b}' '{b}'
|
||||
run 0 ../equals '{1[->10,20];b}' '{[*10..20];b}'
|
||||
run 0 ../equals '{1[->..];b}' '{[*1..];b}'
|
||||
run 0 ../equals '{{a&!c}[->0];b}' '{b}'
|
||||
|
|
|
|||
|
|
@ -416,28 +416,32 @@ namespace spot
|
|||
|
||||
return;
|
||||
case bunop::Equal:
|
||||
case bunop::Goto:
|
||||
{
|
||||
// b[=min..max] == (!b;b[=min..max]) | (b;b[=min-1..max-1])
|
||||
// b[=0..max] == [*0] | (!b;b[=0..max]) | (b;b[=0..max-1])
|
||||
// Note: b[=0] == (!b)[*] is a trivial identity, so it will
|
||||
// never occur here.
|
||||
|
||||
formula* f1 = // !b;b[min..max]
|
||||
// b[->min..max] == (!b;b[->min..max]) | (b;b[->min-1..max-1])
|
||||
// b[->0..max] == [*0] | (!b;b[->0..max]) | (b;b[->0..max-1])
|
||||
// Note: b[->0] == [*0] is a trivial identity, so it will
|
||||
// never occur here.
|
||||
|
||||
formula* f1 = // !b;b[=min..max] or !b;b[->min..max]
|
||||
multop::instance(multop::Concat,
|
||||
unop::instance(unop::Not,
|
||||
bo->child()->clone()),
|
||||
bo->clone());
|
||||
|
||||
formula* f2 = // b;b[=min-1..max-1]
|
||||
formula* f2 = // b;b[=min-1..max-1] or b;b[->min-1..max-1]
|
||||
multop::instance(multop::Concat,
|
||||
bo->child()->clone(),
|
||||
bunop::instance(bunop::Equal,
|
||||
bunop::instance(op,
|
||||
bo->child()->clone(),
|
||||
min2, max2));
|
||||
f = multop::instance(multop::Or, f1, f2);
|
||||
|
||||
res_ = recurse_and_concat(f);
|
||||
|
||||
f->destroy();
|
||||
if (min == 0)
|
||||
res_ |= now_to_concat();
|
||||
|
|
|
|||
|
|
@ -84,6 +84,7 @@ check_psl '{(a* & (c;b*) & d);e}'
|
|||
check_psl '{[*2];a[*2..4]}|->b'
|
||||
check_psl '{a[*2..5] && b[*..3]}|->c'
|
||||
check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c'
|
||||
check_psl '{(a[->3]) & {[+];b}}<>->c'
|
||||
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
|
||||
# Ruah, Zarpas (2007).
|
||||
check_psl '{[*];req;ack}|=>{start;busy[*];done}'
|
||||
|
|
@ -92,6 +93,8 @@ check_psl '{[*];req;ack}|=>{start;busy[*];done}'
|
|||
check_psl '{end[=3]}(false)' # 2.27.A
|
||||
check_psl '{[*]; {read[=3]} && {write[=2]}} |=>
|
||||
{(!read && !write)[*]; ready}' # 3.5.A
|
||||
check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp;
|
||||
{status_valid[->]} && {stop[=0]; true}} |-> {!data_out}' # 2.33
|
||||
|
||||
|
||||
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue