From 6e8af75ee9e64de7636167820680274f1578d401 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 21 May 2018 15:17:18 +0200 Subject: [PATCH] autcross: exercise %S, %L, and {name{nest}} * tests/core/autcross.test, tests/core/autcross2.test: More tests. --- tests/core/autcross.test | 13 ++++++++----- tests/core/autcross2.test | 5 +++-- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/tests/core/autcross.test b/tests/core/autcross.test index 87bace1d2..2ac14eb34 100755 --- a/tests/core/autcross.test +++ b/tests/core/autcross.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -24,17 +24,20 @@ set -e # Skip this test if ltl2dstar is not installed. (ltl2dstar --version) || exit 77 +# The {autfilt {complement}} name makes sure we can nest braces. randaut -n10 2 | -autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ + autcross 'ltl2dstar --complement-input=yes' \ + '{autfilt {complement}} autfilt --complement' \ --csv=out.csv 2>stderr # 5 lines per input automaton, and 1 "No problem detected" line. test 51 = `wc -l < stderr` grep -q 'sanity check' stderr -# --no-check still allows to build a CSV +# --no-check still allows to build a CSV. Exercise %S. randaut -n10 2 | -autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ + autcross 'ltl2dstar --complement-input=yes' \ + '{autfilt {complement}} autfilt --complement %S>%O' \ --csv=out2.csv --no-check 2>stderr test 51 = `wc -l < stderr` grep -q 'sanity check' stderr && exit 1 diff --git a/tests/core/autcross2.test b/tests/core/autcross2.test index 81e037cd1..c7ba9a36d 100755 --- a/tests/core/autcross2.test +++ b/tests/core/autcross2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -21,8 +21,9 @@ . ./defs set -e +# Exercise %L while we are at it. randaut -n10 2 | tee input | -autcross --language-preserve 'autfilt' 'autfilt --complement' \ +autcross --language-preserve 'autfilt %L>%O' 'autfilt --complement' \ --save-bogus=bogus.hoa 2>stderr && exit 1 cat stderr # We should have 4 counterexample per input automaton