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

use ltl2tgba -Ds instead of ltl2tgba -sD in the test suite

Because -s can now take arguments.

* src/tgbatest/ltl2dstar2.test: Here.
parent 1578cdf8
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et
# Copyright (C) 2013, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -71,7 +71,7 @@ head -n 20 > formulas
while read f; do
expected=`$ltl2tgba "$f" -BD --stats '%s %e 1 %d'`
$ltlfilt -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - foo
ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - foo
echo "$f"
output=`$dstar2tgba foo -BD --stats '%s %e %d 1'`
# the '1 %d' matching '%d 1' makes sure input and output are deterministic.
......
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