alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Introduce [=min..max] operator.

Browse source 
* src/ltlast/bunop.hh: Declare bunop::Equal
* 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::Equal in
the translation.
* src/ltltest/equals.test: Test trivial identities
for [=min..max].
* src/tgbatest/ltl2tgba.test: Add new formulae to test.
This commit is contained in:
Alexandre Duret-Lutz 2010-10-14 18:51:34 +02:00
parent d7781bc4d6
commit 8d4a413a37
7 changed files with 236 additions and 91 deletions
Download patch file Download diff file Expand all files Collapse all files

186
src/ltlast/bunop.cc
View file

@ -24,6 +24,8 @@
#include <iostream>
#include <sstream>
#include "constant.hh"
#include "unop.hh"
#include "ltlvisit/kind.hh"
namespace spot
{
@ -107,6 +109,8 @@ namespace spot
{
switch (op_)
{
case Equal:
return "Equal";
case Star:
return "Star";
}
@ -120,14 +124,22 @@ namespace spot
{
std::ostringstream out;
// Syntactic sugaring
if (min_ == 1 && max_ == unbounded)
switch (op_)
{
out << "[+]";
return out.str();
case Star:
// Syntactic sugaring
if (min_ == 1 && max_ == unbounded)
{
out << "[+]";
return out.str();
}
out << "[*";
break;
case Equal:
out << "[=";
break;
}
out << "[*";
if (min_ != 0 || max_ != unbounded)
{
out << min_;
@ -151,73 +163,115 @@ namespace spot
// Some trivial simplifications.
// - [*0][*min..max] = [*0]
if (child == constant::empty_word_instance())
return child;
// - 0[*0..max] = [*0]
// - 0[*min..max] = 0 if min > 0
if (child == constant::false_instance())
switch (op)
{
if (min == 0)
return constant::empty_word_instance();
else
return child;
}
case Equal:
{
// - 0[=0..max] = [*]
// - 0[=min..max] = 0 if min > 0
if (child == constant::false_instance())
{
if (min == 0)
{
max = -1U;
op = Star;
child = constant::true_instance();
break;
}
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] = (!Exp)[*]
if (max == 0)
return bunop::instance(bunop::Star,
unop::instance(unop::Not, child));
break;
}
case Star:
{
// - [*0][*min..max] = [*0]
if (child == constant::empty_word_instance())
return child;
// - Exp[*0..0] = [*0]
if (max == 0)
{
child->destroy();
return constant::empty_word_instance();
}
// - 0[*0..max] = [*0]
// - 0[*min..max] = 0 if min > 0
if (child == constant::false_instance())
{
if (min == 0)
return constant::empty_word_instance();
else
return child;
}
// - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] if i*(min+1)<=j(min)+1.
bunop* s = dynamic_cast<bunop*>(child);
if (s)
{
unsigned i = s->min();
unsigned j = s->max();
// - Exp[*0] = [*0]
if (max == 0)
{
child->destroy();
return constant::empty_word_instance();
}
// Exp has to be true between i*min and j*min
// then between i*(min+1) and j*(min+1)
// ...
// finally between i*max and j*max
//
// We can merge these intervals into [i*min..j*max] iff the
// first are adjacent or overlap, i.e. iff
// i*(min+1) <= j*min+1.
// (Because i<=j, this entails that the other intervals also
// overlap).
// - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)]
// if i*(min+1)<=j(min)+1.
bunop* s = dynamic_cast<bunop*>(child);
if (s)
{
unsigned i = s->min();
unsigned j = s->max();
formula* exp = s->child();
if (j == unbounded)
{
min *= i;
max = unbounded;
// Exp has to be true between i*min and j*min
// then between i*(min+1) and j*(min+1)
// ...
// finally between i*max and j*max
//
// We can merge these intervals into [i*min..j*max] iff the
// first are adjacent or overlap, i.e. iff
// i*(min+1) <= j*min+1.
// (Because i<=j, this entails that the other intervals also
// overlap).
// Exp[*min..max]
exp->clone();
child->destroy();
child = exp;
}
else
{
if (i * (min + 1) <= (j * min) + 1)
{
min *= i;
if (max != unbounded)
{
if (j == unbounded)
max = unbounded;
else
max *= j;
}
exp->clone();
child->destroy();
child = exp;
}
}
formula* exp = s->child();
if (j == unbounded)
{
min *= i;
max = unbounded;
// Exp[*min..max]
exp->clone();
child->destroy();
child = exp;
}
else
{
if (i * (min + 1) <= (j * min) + 1)
{
min *= i;
if (max != unbounded)
{
if (j == unbounded)
max = unbounded;
else
max *= j;
}
exp->clone();
child->destroy();
child = exp;
}
}
}
break;
}
}
pair p(pairo(op, child), pairu(min, max));

8
src/ltlast/bunop.hh
View file

@ -37,7 +37,7 @@ namespace spot
class bunop : public ref_formula
{
public:
enum type { Star };
enum type { Star, Equal };
static const unsigned unbounded = -1U;
@ -49,7 +49,13 @@ namespace spot
/// - 0[*0..max] = [*0]
/// - 0[*min..max] = 0 if min > 0
/// - [*0][*min..max] = [*0]
/// - Exp[*0] = [*0]
/// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1.
/// - 0[=0..max] = 1[*]
/// - 0[=min..max] = 0 if min > 0
/// - 1[=0] = [*0]
/// - 1[=min..max] = 1[*min..max] if max > 0
/// - Exp[=0] = (!Exp)[*]
///
/// These rewriting rules imply that it is not possible to build
/// an LTL formula object that is SYNTACTICALLY equal to one of

66
src/ltlparse/ltlparse.yy
View file

@ -35,6 +35,7 @@
#include <string>
#include "public.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/kind.hh"
struct minmax_t { unsigned min, max; };
}
@ -92,9 +93,10 @@ using namespace spot::ltl;
%token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator"
%token OP_PLUS "plus operator"
%token OP_STAR_OPEN "opening bracket for star operator"
%token OP_STAR_CLOSE "closing bracket for star operator"
%token <num> OP_STAR_NUM "number for star operator"
%token OP_STAR_SEP "separator for star operator"
%token OP_EQUAL_OPEN "opening bracket for equal 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"
%token OP_UCONCAT "universal concat operator"
%token OP_ECONCAT "existential concat operator"
%token OP_UCONCAT_NONO "universal non-overlapping concat operator"
@ -124,7 +126,7 @@ using namespace spot::ltl;
%nonassoc OP_X
/* High priority regex operator. */
%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS
%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN
/* Not has the most important priority after Wring's `=0' and `=1'. */
%nonassoc OP_NOT
@ -133,7 +135,7 @@ using namespace spot::ltl;
%type <ltl> subformula booleanatom rationalexp
%type <ltl> bracedrationalexp parenthesedsubformula
%type <minmax> starargs
%type <minmax> starargs equalargs sqbracketargs
%destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl>
@ -187,24 +189,27 @@ enderror: error END_OF_INPUT
}
OP_STAR_SEP_opt: | OP_STAR_SEP
OP_SQBKT_SEP_opt: | OP_SQBKT_SEP
error_opt: | error
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
{ $$.min = $1; $$.max = bunop::unbounded; }
| OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
{ $$.min = 0U; $$.max = $2; }
| OP_SQBKT_SEP_opt OP_SQBKT_CLOSE
{ $$.min = 0U; $$.max = bunop::unbounded; }
| OP_SQBKT_NUM OP_SQBKT_CLOSE
{ $$.min = $$.max = $1; }
starargs: OP_STAR
{ $$.min = 0U; $$.max = bunop::unbounded; }
| OP_PLUS
{ $$.min = 1U; $$.max = bunop::unbounded; }
| OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE
{ $$.min = $2; $$.max = $4; }
| OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_CLOSE
{ $$.min = $2; $$.max = bunop::unbounded; }
| OP_STAR_OPEN OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE
{ $$.min = 0U; $$.max = $3; }
| OP_STAR_OPEN OP_STAR_SEP_opt OP_STAR_CLOSE
{ $$.min = 0U; $$.max = bunop::unbounded; }
| OP_STAR_OPEN OP_STAR_NUM OP_STAR_CLOSE
{ $$.min = $$.max = $2; }
| OP_STAR_OPEN error OP_STAR_CLOSE
| OP_STAR_OPEN sqbracketargs
{ $$ = $2; }
| OP_STAR_OPEN error OP_SQBKT_CLOSE
{ error_list.push_back(parse_error(@$,
"treating this star block as [*]"));
$$.min = 0U; $$.max = bunop::unbounded; }
@ -213,6 +218,17 @@ starargs: OP_STAR
"missing closing bracket for star"));
$$.min = $$.max = 0U; }
equalargs: OP_EQUAL_OPEN sqbracketargs
{ $$ = $2; }
| OP_EQUAL_OPEN error OP_SQBKT_CLOSE
{ error_list.push_back(parse_error(@$,
"treating this star 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"));
$$.min = $$.max = 0U; }
/* The reason we use `constant::false_instance()' for error recovery
is that it isn't reference counted. (Hence it can't leak references.) */
@ -323,6 +339,22 @@ rationalexp: booleanatom
| starargs
{ $$ = bunop::instance(bunop::Star, constant::true_instance(),
$1.min, $1.max); }
| rationalexp equalargs
{
if ((kind_of($1) & Boolean_Kind) == Boolean_Kind)
{
$$ = bunop::instance(bunop::Equal, $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"));
$$ = constant::false_instance();
}
}
bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE
{ $$ = $2; }

13
src/ltlparse/ltlscan.ll
View file

@ -59,7 +59,7 @@ flex_set_buffer(const char* buf, int start_tok)
%}
%s not_prop
%x star
%x sqbracket
%%
@ -96,14 +96,15 @@ flex_set_buffer(const char* buf, int start_tok)
":" BEGIN(0); return token::OP_FUSION;
"*"|"[*]" BEGIN(0); return token::OP_STAR;
"[+]" BEGIN(0); return token::OP_PLUS;
"[*" BEGIN(star); return token::OP_STAR_OPEN;
<star>"]" BEGIN(0); return token::OP_STAR_CLOSE;
<star>[0-9]+ {
"[*" BEGIN(sqbracket); return token::OP_STAR_OPEN;
"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
<sqbracket>"]" BEGIN(0); return token::OP_SQBKT_CLOSE;
<sqbracket>[0-9]+ {
unsigned num = 0;
try {
num = boost::lexical_cast<unsigned>(yytext);
yylval->num = num;
return token::OP_STAR_NUM;
return token::OP_SQBKT_NUM;
}
catch (boost::bad_lexical_cast &)
{
@ -114,7 +115,7 @@ flex_set_buffer(const char* buf, int start_tok)
yylloc->step();
}
}
<star>","|".." return token::OP_STAR_SEP;
<sqbracket>","|".." return token::OP_SQBKT_SEP;
/* & and | come from Spin. && and || from LTL2BA.

11
src/ltltest/equals.test
View file

@ -139,3 +139,14 @@ run 0 ../equals '{a[+][*1..3]}' '{a[+]}'
run 0 ../equals '{a[*1..3][+]}' '{a[+]}'
run 0 ../equals '{[*2][+]}' '{[*2][+]}'
run 0 ../equals '{[+][*2]}' '{[*2..]}'
run 0 ../equals '{0[=2]}' '0'
run 0 ../equals '{0[=2..]}' '0'
run 0 ../equals '{0[=1..10]}' '0'
run 0 ../equals '{0[=0]}' '{[*]}'
run 0 ../equals '{0[=0..10]}' '{*}'
run 0 ../equals '{0[=0..]}' '{*}'
run 0 ../equals '{1[=0]}' '{[*0]}'
run 0 ../equals '{1[=1..2]}' '{[*1..2]}'
run 0 ../equals '{1[=..4]}' '{1[*..4]}'
run 0 ../equals '{b[=0]}' '{(!b)[*]}'

37
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -233,6 +233,9 @@ namespace spot
std::ostream&
trace_ltl_bdd(const translate_dict& d, bdd f)
{
std::cerr << "Displaying BDD ";
bdd_print_set(std::cerr, d.dict, f) << ":" << std::endl;
minato_isop isop(f);
bdd cube;
while ((cube = isop.next()) != bddfalse)
@ -318,7 +321,7 @@ namespace spot
bdd next_to_concat()
{
if (!to_concat_)
to_concat_ = constant::empty_word_instance();
return bddtrue;
int x = dict_.register_next_variable(to_concat_);
return bdd_ithvar(x);
}
@ -391,6 +394,9 @@ namespace spot
formula* f;
unsigned min = bo->min();
unsigned max = bo->max();
assert(max > 0);
unsigned min2 = (min == 0) ? 0 : (min - 1);
unsigned max2 =
(max == bunop::unbounded) ? bunop::unbounded : (max - 1);
@ -407,7 +413,36 @@ namespace spot
res_ = recurse(bo->child(), f);
if (min == 0)
res_ |= now_to_concat();
return;
case bunop::Equal:
{
// 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]
multop::instance(multop::Concat,
unop::instance(unop::Not,
bo->child()->clone()),
bo->clone());
formula* f2 = // b;b[=min-1..max-1]
multop::instance(multop::Concat,
bo->child()->clone(),
bunop::instance(bunop::Equal,
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();
return;
}
}
/* Unreachable code. */
assert(0);

6
src/tgbatest/ltl2tgba.test
View file

@ -87,6 +87,12 @@ check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c'
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
# Ruah, Zarpas (2007).
check_psl '{[*];req;ack}|=>{start;busy[*];done}'
# Examples from "Property-by-Example Guide: a Handbook of PSL Examples"
# by Ben David and Orni (2005)/
check_psl '{end[=3]}(false)' # 2.27.A
check_psl '{[*]; {read[=3]} && {write[=2]}} |=>
{(!read && !write)[*]; ready}' # 3.5.A
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.