Commit 7144efab authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

hoa: add option to output version 1.1

* spot/twaalgos/hoa.cc: Implement the option.
* bin/common_aoutput.cc, doc/org/hoa.org,
doc/org/oaut.org, spot/twaalgos/hoa.hh, NEWS: Document it.
* tests/core/strength.test: Test that.
parent fd33eedf
New in spot 2.0a (not yet released)
Library:
* The print_hoa() function will now output version 1.1 of the HOA
format when passed the "1.1" option (i.e., use -H1.1 from any
command-line tool). As far as Spot is concerned, this allows
negated properties to be expressed. Version 1 of the HOA format
is still the default, but we plan to default to version 1.1 in the
future.
Bug fixes:
* Typo in documentation of the -H option in --help output.
......
......@@ -101,8 +101,9 @@ static const argp_option options[] =
"(+INT) add INT to all set numbers, "
"(<INT) display at most INT states, "
"(#) show internal edge numbers", 0 },
{ "hoaf", 'H', "i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
{ "hoaf", 'H', "1.1|i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
"Output the automaton in HOA format (default). Add letters to select "
"(1.1) version 1.1 of the format, "
"(i) use implicit labels for complete deterministic automata, "
"(s) prefer state-based acceptance when possible [default], "
"(t) force transition-based acceptance, "
......
......@@ -21,6 +21,13 @@ some information that are useful to better understand the behavior
of the tools distributed by Spot, and it also look at some lower-level,
discussing details that are interesting when programming with Spot.
Spot can read files written using either version 1 or version 1.1 of
the HOA format. It currently outputs version 1 by default, but
version 1.1 can be requested from the command-line using option
=-H1.1=. Future version of Spot are likely to switch to version 1.1
of HOA by default, so version 1 can already be requested explicitly
using =-H1=.
* Format, files, and TωA
Some note about the abbreviation first. We usually write "HOA format"
......@@ -48,6 +55,9 @@ the HOA format, the output may not be exactly the same as the input.
deterministic" or "deterministic") automata are currently supported
by Spot.
- Automata using explicit alphabet (introduced in version 1.1 of the format
via =Alphabet:=) are not supported.
- The maximum number of acceptance sets used is (currently) limited
to 32.
......@@ -672,6 +682,14 @@ particular:
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= |
| =colored= | ignored | no | checked | |
The above table is for version 1 of the format. When version 1.1 is
selected (using =-H1.1=), some negated properties may be output. In
particular, =stutter-sensitive= is replaced by =!stutter-invariant=.
The logic of not cluttering the output with all of =!terminal=,
=!weak=, and =!inhenrently-weak= is similar to the positive versions:
=!inherently-weak= implies =!weak= which in turn implies =!terminal=,
so only one of those is emitted unless =-Hv= is used.
** Named properties
In addition to the bit properties discussed above, a TωA can carry
......
......@@ -391,6 +391,53 @@ HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptanc
HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc stutter-invariant --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END--
#+END_SRC
Finally, version 1.1 of the HOA format can be specified using the
=-H1.1= option. Version 1, which is currently the default, can also
be requested explicitly using =-H1=. The main advantage of version
1.1, as far as Spot is concerned, is that some of negated properties
can be transmitted. For instance, compare
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -f GFa -f FGa -H1 --check | grep -E '^(HOA|properties|name):'
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
name: "GFa"
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
HOA: v1
name: "FGa"
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: weak
#+END_SRC
versus
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -f GFa -f FGa -H1.1 --check | grep -E '^(HOA|properties|name):'
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1.1
name: "GFa"
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant !inherently-weak
HOA: v1.1
name: "FGa"
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic !unambiguous stutter-invariant weak
properties: !terminal
#+END_SRC
The =--check= option inspects the automata for additional properties
such that their strength or whether they are stutter-invariant and
unambiguous. You can see in this example that version 1.1 of the
format carries additional negated properties that could not be
represented in the first version.
* LBTT output
The [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output has two flavors: state-based (which is used to output
......
......@@ -252,12 +252,29 @@ namespace spot
bool implicit_labels = false;
bool verbose = false;
bool state_labels = false;
bool v1_1 = false;
if (opt)
while (*opt)
{
switch (char c = *opt++)
{
case '1':
if (opt[0] == '.' && opt[1] == '1')
{
v1_1 = true;
opt += 2;
}
else if (opt[0] == '.' && opt[1] == '0')
{
v1_1 = false;
opt += 2;
}
else
{
v1_1 = false;
}
break;
case 'i':
implicit_labels = true;
break;
......@@ -297,7 +314,7 @@ namespace spot
unsigned num_states = aut->num_states();
const char nl = newline ? '\n' : ' ';
os << "HOA: v1" << nl;
os << (v1_1 ? "HOA: v1.1" : "HOA: v1") << nl;
auto n = aut->get_named_prop<std::string>("automaton-name");
if (n)
escape_str(os << "name: \"", *n) << '"' << nl;
......@@ -423,10 +440,16 @@ namespace spot
prop(" trans-acc");
if (md.is_colored)
prop(" colored");
else if (verbose && v1_1)
prop(" !colored");
if (md.is_complete)
prop(" complete");
else if (v1_1)
prop(" !complete");
if (md.is_deterministic)
prop(" deterministic");
else if (v1_1)
prop(" !deterministic");
// Deterministic automata are also unambiguous, so writing both
// properties seems redundant. People working on unambiguous
// automata are usually concerned about non-deterministic
......@@ -434,16 +457,29 @@ namespace spot
// in the case of deterministic automata.
if (aut->prop_unambiguous() && (verbose || !md.is_deterministic))
prop(" unambiguous");
else if (v1_1 && !aut->prop_unambiguous())
prop(" !unambiguous");
if (aut->prop_stutter_invariant())
prop(" stutter-invariant");
if (!aut->prop_stutter_invariant())
prop(" stutter-sensitive");
{
if (v1_1)
prop(" !stutter-invariant");
else
prop(" stutter-sensitive");
}
if (aut->prop_terminal())
prop(" terminal");
if (aut->prop_weak() && (verbose || aut->prop_terminal() != true))
prop(" weak");
if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true))
prop(" inherently-weak");
if (v1_1 && !aut->prop_terminal() && (aut->prop_weak() || verbose))
prop(" !terminal");
if (v1_1 && !aut->prop_weak() && (aut->prop_inherently_weak() || verbose))
prop(" !weak");
if (v1_1 && !aut->prop_inherently_weak())
prop(" !inherently-weak");
os << nl;
// If we want to output implicit labels, we have to
......
......@@ -35,7 +35,8 @@ namespace spot
/// deterministic automata, (k) state labels when possible,
/// (s) state-based acceptance when possible, (t)
/// transition-based acceptance, (m) mixed acceptance, (l)
/// single-line output, (v) verbose properties.
/// single-line output, (v) verbose properties, (1.1) use
/// version 1.1 of the HOA format.
SPOT_API std::ostream&
print_hoa(std::ostream& os,
const const_twa_ptr& g,
......
......@@ -588,4 +588,371 @@ State: 4
EOF
diff out expected
autfilt -q expected
# Test HOA v1.1
autfilt expected -H1.1 --check > out2
cat >expected2 <<EOF
HOA: v1.1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 2
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 4
Start: 0
AP: 2 "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0
[!0&!1] 0
[0&!1] 1
[1] 2
State: 1
[!0&!1] 0
[0&!1] 1
[!0&1] 2
[0&1] 3
State: 2 {0}
[t] 2
State: 3
[!0] 2
[0] 3
--END--
HOA: v1.1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored !complete
properties: deterministic stutter-invariant weak !terminal
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1.1
States: 3
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic !unambiguous weak !terminal
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0
[1&!2] 2
State: 1 {0}
[0] 1
State: 2
[!1&!2] 0
[1&!2] 2
--END--
HOA: v1.1
States: 2
Start: 0
AP: 2 "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc !complete
properties: deterministic stutter-invariant !inherently-weak
--BODY--
State: 0
[!0&!1] 0 {0}
[0&!1] 1
State: 1
[!0&!1] 0 {0}
[0&!1] 1
--END--
HOA: v1.1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 2
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored !complete
properties: deterministic stutter-invariant weak !terminal
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1.1
States: 5
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic !unambiguous weak !terminal
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0
[1&!2] 2
[2] 3
State: 1 {0}
[0] 1
State: 2
[!1&!2] 0
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3 {0}
[t] 3
State: 4
[!1] 3
[1] 4
--END--
HOA: v1.1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored !complete
properties: deterministic stutter-invariant weak !terminal
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1.1
States: 3
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc !complete
properties: !deterministic !unambiguous !inherently-weak
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0 {0}
[1&!2] 2
State: 1
[0] 1 {0}
State: 2
[!1&!2] 0 {0}
[1&!2] 2
--END--
HOA: v1.1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant inherently-weak !weak
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
--END--
HOA: v1.1
States: 2
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[t] 0
--END--
HOA: v1.1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored !complete
properties: deterministic stutter-invariant weak !terminal
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1.1
States: 5
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc !complete
properties: !deterministic !unambiguous !inherently-weak
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0 {0}
[1&!2] 2
[2] 3
State: 1
[0] 1 {0}
State: 2
[!1&!2] 0 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
EOF
diff out2 expected2
# Make sure no property are lost
autfilt -H1.1 out2 > out3
diff out3 expected2
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