hoa: add support for unlabeled transitions
* src/hoaparse/hoaparse.yy: Here. * src/tgbatest/hoaparse.test: Add tests.
This commit is contained in:
Alexandre Duret-Lutz
parent
1d962f79ac
commit
69678152b6
2 changed files with 185 additions and 27 deletions
|
|
@ -45,6 +45,8 @@
|
|||
spot::hoa_aut_ptr h;
|
||||
spot::ltl::environment* env;
|
||||
std::vector<int> ap;
|
||||
std::vector<bdd> guards;
|
||||
std::vector<bdd>::const_iterator cur_guard;
|
||||
spot::location states_loc;
|
||||
spot::location ap_loc;
|
||||
spot::location state_label_loc;
|
||||
|
|
@ -59,7 +61,6 @@
|
|||
bdd state_label;
|
||||
bdd cur_label;
|
||||
bool has_state_label = false;
|
||||
bool has_trans_label = false;
|
||||
bool ignore_more_ap = false; // Set to true after the first "AP:"
|
||||
// line has been read.
|
||||
bool ignore_acc = false; // Set to true in case of missing
|
||||
|
|
@ -92,6 +93,8 @@
|
|||
We must ensure that YYSTYPE is declared (by the above %union)
|
||||
before parsedecl.hh uses it. */
|
||||
#include "parsedecl.hh"
|
||||
|
||||
static void fill_guards(result_& res);
|
||||
}
|
||||
|
||||
%token HOA "HOA:"
|
||||
|
|
@ -446,7 +449,16 @@ state-num: INT
|
|||
}
|
||||
|
||||
states: | states state
|
||||
state: state-name edges
|
||||
state: state-name labeled-edges
|
||||
| state-name unlabeled-edges
|
||||
{
|
||||
if (!res.has_state_label)
|
||||
{
|
||||
if (res.cur_guard != res.guards.end())
|
||||
error(@$, "not enough transitions for this state");
|
||||
res.cur_guard = res.guards.begin();
|
||||
}
|
||||
}
|
||||
state-name: "State:" state-label_opt state-num string_opt acc-sig_opt
|
||||
{
|
||||
res.cur_state = $3;
|
||||
|
|
@ -461,19 +473,14 @@ state-label_opt: { res.has_state_label = false; }
|
|||
| label { res.has_state_label = true;
|
||||
res.state_label_loc = @1;
|
||||
res.state_label = res.cur_label; }
|
||||
trans-label_opt: { res.has_trans_label = false; }
|
||||
| label
|
||||
trans-label: label
|
||||
{
|
||||
if (res.has_state_label)
|
||||
{
|
||||
error(@1, "cannot label this transition because...");
|
||||
error(res.state_label_loc,
|
||||
"... the state is already labeled.");
|
||||
res.has_trans_label = false;
|
||||
}
|
||||
else
|
||||
{
|
||||
res.has_trans_label = true;
|
||||
res.cur_label = res.state_label;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -503,27 +510,72 @@ acc-sets:
|
|||
else
|
||||
$$ = $1 | res.h->aut->acc().mark($2);
|
||||
}
|
||||
edges: | edges edge
|
||||
edge: trans-label_opt state-num acc-sig_opt
|
||||
{
|
||||
bdd cond = bddfalse;
|
||||
if (res.has_state_label)
|
||||
cond = res.state_label;
|
||||
else if (res.has_trans_label)
|
||||
cond = res.cur_label;
|
||||
else
|
||||
error(@$, "unlabeled transitions are not yet supported");
|
||||
res.h->aut->new_transition(res.cur_state, $2, cond,
|
||||
$3 | res.acc_state);
|
||||
}
|
||||
| trans-label_opt state-conj-2 acc-sig_opt
|
||||
{
|
||||
error(@2, "alternation is not yet supported");
|
||||
YYABORT;
|
||||
}
|
||||
labeled-edges: | labeled-edges labeled-edge
|
||||
labeled-edge: trans-label state-num acc-sig_opt
|
||||
{
|
||||
res.h->aut->new_transition(res.cur_state, $2,
|
||||
res.cur_label, $3 | res.acc_state);
|
||||
}
|
||||
| trans-label state-conj-2 acc-sig_opt
|
||||
{
|
||||
error(@2, "alternation is not yet supported");
|
||||
YYABORT;
|
||||
}
|
||||
|
||||
/* We never have zero unlabeled edges, these are considered as zero
|
||||
labeled edges. */
|
||||
unlabeled-edges: unlabeled-edge | unlabeled-edges unlabeled-edge
|
||||
unlabeled-edge: state-num acc-sig_opt
|
||||
{
|
||||
bdd cond;
|
||||
if (res.has_state_label)
|
||||
{
|
||||
cond = res.state_label;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (res.guards.empty())
|
||||
fill_guards(res);
|
||||
if (res.cur_guard == res.guards.end())
|
||||
{
|
||||
error(@$, "too many transition for this state, "
|
||||
"ignoring this one");
|
||||
cond = bddfalse;
|
||||
}
|
||||
else
|
||||
{
|
||||
cond = *res.cur_guard++;
|
||||
}
|
||||
}
|
||||
res.h->aut->new_transition(res.cur_state, $1,
|
||||
cond, $2 | res.acc_state);
|
||||
}
|
||||
| state-conj-2 acc-sig_opt
|
||||
{
|
||||
error(@1, "alternation is not yet supported");
|
||||
YYABORT;
|
||||
}
|
||||
|
||||
%%
|
||||
|
||||
static void fill_guards(result_& r)
|
||||
{
|
||||
spot::bdd_dict_ptr d = r.h->aut->get_dict();
|
||||
unsigned nap = r.ap.size();
|
||||
|
||||
int* vars = new int[nap];
|
||||
for (unsigned i = 0; i < nap; ++i)
|
||||
vars[i] = r.ap[nap - 1 - i];
|
||||
|
||||
// build the 2^nap possible guards
|
||||
r.guards.reserve(1U << nap);
|
||||
for (size_t i = 0; i < (1U << nap); ++i)
|
||||
r.guards.push_back(bdd_ibuildcube(i, nap, vars));
|
||||
r.cur_guard = r.guards.begin();
|
||||
|
||||
delete[] vars;
|
||||
}
|
||||
|
||||
void
|
||||
hoayy::parser::error(const location_type& location,
|
||||
const std::string& message)
|
||||
|
|
|
|||
|
|
@ -32,6 +32,15 @@ expecterr()
|
|||
diff $1.err $1.exp
|
||||
}
|
||||
|
||||
expectok()
|
||||
{
|
||||
cat >$1.exp
|
||||
../../bin/autfilt --hoa $1 >$1.out
|
||||
test $? = 0
|
||||
cat $1.out
|
||||
diff $1.out $1.exp
|
||||
}
|
||||
|
||||
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
|
|
@ -175,6 +184,7 @@ input:9.11: number is larger than the count of acceptance sets...
|
|||
input:5.1-13: ... declared here.
|
||||
EOF
|
||||
|
||||
# Let's have two broken automata in a row...
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
Start: 0
|
||||
|
|
@ -198,3 +208,99 @@ input:5.1-13: ... declared here.
|
|||
input:12.1-7: unsupported version of the HOA format
|
||||
input:12.1-7: missing 'Acceptance:' header
|
||||
EOF
|
||||
|
||||
cat >input<<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 (Inf(0) & Inf(1))
|
||||
AP: 2 "a" "b"
|
||||
--BODY--
|
||||
State: 0 "foo" { 0 }
|
||||
2 /* !a & !b */
|
||||
0 /* a & !b */
|
||||
1 /* !a & b */
|
||||
1 /* a & b */
|
||||
State: 1 { 1 }
|
||||
1 1 1 1 /* four transitions on one line */
|
||||
State: 2 "sink state" { 0 }
|
||||
2 2 2 2
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expectok input <<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 Inf(0)&Inf(1)
|
||||
properties: trans-labels explicit-labels state-acc complete deterministic
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[!0&!1] 1
|
||||
[0&!1] 0
|
||||
[!0&1] 2
|
||||
[0&1] 2
|
||||
State: 1 {0}
|
||||
[!0&!1] 1
|
||||
[0&!1] 1
|
||||
[!0&1] 1
|
||||
[0&1] 1
|
||||
State: 2 {1}
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
[!0&1] 2
|
||||
[0&1] 2
|
||||
--END--
|
||||
EOF
|
||||
|
||||
cat >input<<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 (Inf(0) & Inf(1))
|
||||
AP: 2 "a" "b"
|
||||
--BODY--
|
||||
State: 0 "foo" { 0 }
|
||||
2 /* !a & !b */
|
||||
0 /* a & !b */
|
||||
1 /* !a & b */
|
||||
/* missing transition */
|
||||
State: 1 { 1 }
|
||||
1 1 1 1 /* four transitions on one line */
|
||||
State: 2 "sink state" { 0 }
|
||||
2 2 2 2
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:8.5-11.7: not enough transitions for this state
|
||||
EOF
|
||||
|
||||
cat >input<<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 (Inf(0) & Inf(1))
|
||||
AP: 2 "a" "b"
|
||||
--BODY--
|
||||
State: 0 "foo" { 0 }
|
||||
2 /* !a & !b */
|
||||
0 /* a & !b */
|
||||
1 /* !a & b */
|
||||
1 /* a & b */
|
||||
2 /* extra transition ! */
|
||||
State: 1 { 1 }
|
||||
1 1 1 1 /* four transitions on one line */
|
||||
State: 2 "sink state" { 0 }
|
||||
2 2 2 2
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:13.7: too many transition for this state, ignoring this one
|
||||
EOF
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue