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

hoa: add alias support

Browse source 
* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-21 11:05:24 +01:00
parent 691ab05926
commit 7a03228880
2 changed files with 83 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/hoaparse/hoaparse.yy
View file

@ -32,6 +32,7 @@
#include <string>
#include <cstring>
#include <sstream>
#include <unordered_map>
#include "ltlast/constant.hh"
#include "public.hh"
@ -48,6 +49,7 @@
std::vector<bdd> guards;
std::vector<bdd>::const_iterator cur_guard;
std::vector<bool> declared_states; // States that have been declared.
std::unordered_map<std::string, bdd> alias;
spot::location states_loc;
spot::location ap_loc;
spot::location state_label_loc;
@ -238,6 +240,12 @@ header-item: "States:" INT
}
| "Alias:" ANAME label-expr
{
if (!res.alias.emplace(*$2, bdd_from_int($3)).second)
{
std::ostringstream o;
o << "ignoring redefinition of alias @" << *$2;
error(@$, o.str());
}
delete $2;
bdd_delref($3);
}
@ -352,10 +360,18 @@ label-expr: 't'
}
| ANAME
{
auto i = res.alias.find(*$1);
if (i == res.alias.end())
{
error(@$, "unknown alias @" + *$1);
$$ = 1;
}
else
{
$$ = i->second.id();
bdd_addref($$);
}
delete $1;
error(@1, "aliases are not yet supported");
YYABORT;
$$ = 0;
}
| '!' label-expr
{

64
src/tgbatest/hoaparse.test
View file

@ -322,3 +322,67 @@ EOF
expecterr input <<EOF
input:13.7: too many transition for this state, ignoring this one
EOF
cat >input <<EOF
HOA: v1
name: "GFa & GF(b & c)"
States: 1
Start: 0
acc-name: generalized-Buchi 2
Acceptance: 2 (Inf(0) & Inf(1))
AP: 3 "a" "b" "c"
Alias: @a 0
Alias: @a 1 & 2 /* should be @bc */
--BODY--
State: 0
[!@a & !@bc] 0
[@a & !@bc] 0 {0}
[!@a & @bc] 0 {1}
[@a & @bc] 0 {0 1}
--END--
EOF
expecterr input <<EOF
input:9.5-19: ignoring redefinition of alias @a
input:12.13-15: unknown alias @bc
input:13.12-14: unknown alias @bc
input:14.12-14: unknown alias @bc
input:15.11-13: unknown alias @bc
EOF
cat >input <<EOF
HOA: v1
name: "GFa & GF(b & c)"
States: 1
Start: 0
acc-name: generalized-Buchi 2
Acceptance: 2 (Inf(0) & Inf(1))
AP: 3 "a" "b" "c"
Alias: @a 0
Alias: @bc 1 & 2
--BODY--
State: 0
[!@a & !@bc] 0
[@a & !@bc] 0 {0}
[!@a & @bc] 0 {1}
[@a & @bc] 0 {0 1}
--END--
EOF
expectok input <<EOF
HOA: v1
States: 1
Start: 0
AP: 3 "a" "b" "c"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
[!0&!1 | !0&!2] 0
[0&!1 | 0&!2] 0 {0}
[!0&1&2] 0 {1}
[0&1&2] 0 {0 1}
--END--
EOF