Commit 34b798e1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoaparse: validate use of state-labels and trans-labels

* src/hoaparse/hoaparse.yy: Fix a map with properties, and use it to
report error when state-label or trans-label are misused.
* src/tgbatest/hoaparse.test: Test that.
parent eff4bdb8
/* -*- coding: utf-8 -*-
** Copyright (C) 2014 Laboratoire de Recherche et Développement
** Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
** de l'Epita (LRDE).
**
** This file is part of Spot, a model checking library.
......@@ -54,6 +54,8 @@
// chance to reach the end of the current automaton in order to
// process the next one. Several variables below are used to keep
// track of various error conditions.
enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels };
struct result_
{
spot::hoa_aut_ptr h;
......@@ -67,6 +69,7 @@
std::vector<bool> declared_states; // States that have been declared.
std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
std::unordered_map<std::string, bdd> alias;
std::unordered_map<std::string, spot::location> props;
spot::location states_loc;
spot::location ap_loc;
spot::location state_label_loc;
......@@ -89,6 +92,8 @@
bool ignore_more_acc = false; // Set to true after the first
// "Acceptance:" line has been read.
label_style_t label_style = Mixed_Labels;
bool accept_all_needed = false;
bool accept_all_seen = false;
bool aliased_states = false;
......@@ -254,6 +259,29 @@ header: format-version header-items
error(@$, "missing 'Acceptance:' header");
res.ignore_acc = true;
}
// Process properties.
{
auto trans_labels = res.props.find("trans-labels");
auto state_labels = res.props.find("state-labels");
if (trans_labels != res.props.end())
{
if (state_labels == res.props.end())
{
res.label_style = Trans_Labels;
}
else
{
error(trans_labels->second,
"'property: trans-labels' is incompatible with...");
error(state_labels->second,
"... 'property: state-labels'.");
}
}
else if (state_labels != res.props.end())
{
res.label_style = State_Labels;
}
}
}
version: IDENTIFIER
......@@ -417,6 +445,7 @@ acc-spec: | acc-spec BOOLEAN
}
properties: | properties IDENTIFIER
{
res.props.emplace(*$2, @2);
delete $2;
}
header-spec: | header-spec BOOLEAN
......@@ -615,9 +644,21 @@ label: '[' label-expr ']'
res.cur_label = bddtrue;
}
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; }
| label
{
res.has_state_label = true;
res.state_label_loc = @1;
res.state_label = res.cur_label;
if (res.label_style == Trans_Labels)
{
error(@$,
"state label used although the automaton was...");
error(res.props["trans-labels"],
"... declared with 'property: trans-labels' here");
// Do not show this error anymore.
res.label_style = Mixed_Labels;
}
}
trans-label: label
{
if (res.has_state_label)
......@@ -627,6 +668,15 @@ trans-label: label
"... the state is already labeled.");
res.cur_label = res.state_label;
}
if (res.label_style == State_Labels)
{
error(@$, "transition label used although the "
"automaton was...");
error(res.props["state-labels"],
"... declared with 'property: state-labels' here");
// Do not show this error anymore.
res.label_style = Mixed_Labels;
}
}
acc-sig_opt:
......
......@@ -349,6 +349,7 @@ cat >input <<EOF
AP: 3 "a" "b" "c"
Alias: @a 0
Alias: @a 1 & 2 /* should be @bc */
properties: state-labels /* this is bogus */
--BODY--
State: 0
[!@a & !@bc] 0
......@@ -360,10 +361,12 @@ 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:13.13-15: unknown alias @bc
input:13.5-16: transition label used although the automaton was...
input:10.17-28: ... declared with 'property: state-labels' here
input:14.12-14: unknown alias @bc
input:15.11-13: unknown alias @bc
input:15.12-14: unknown alias @bc
input:16.11-13: unknown alias @bc
EOF
cat >input <<EOF
......@@ -685,6 +688,33 @@ State: 2
[t] 2
1 2
--END--
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
properties: trans-labels /* this is bogus */
--BODY--
State: [1] 0 {0} 0
--END--
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
properties: state-labels trans-labels /* this is bogus */
--BODY--
State: [1] 0 {0} 0
--END--
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
properties: state-labels /* OK */
--BODY--
State: [1] 0 {0} 0
--END--
EOF
expecterr input <<EOF
......@@ -692,6 +722,10 @@ input:10.1-4: cannot label this edge because...
input:9.8-10: ... the state is already labeled.
input:14.6: missing label for this edge (previous edge is labeled)
input:17.1-3: ignoring this label, because previous edge has no label
input:27.8-10: state label used although the automaton was...
input:25.13-24: ... declared with 'property: trans-labels' here
input:34.26-37: 'property: trans-labels' is incompatible with...
input:34.13-24: ... 'property: state-labels'.
EOF
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment