ltlcross: disable products columns in CSV if --products=0
* bin/ltlcross.cc: Fix it. * tests/core/ltlcross3.test: Test it. * NEWS: Mention the bug.
This commit is contained in:
parent
b210db8949
commit
c7141bd189
3 changed files with 11 additions and 1 deletions
3
NEWS
3
NEWS
|
|
@ -159,6 +159,9 @@ Bugs fixed:
|
|||
an obligation property, the result would always be a complete
|
||||
automaton even without the -C option.
|
||||
|
||||
* ltlcross --products=0 --csv should not output any product-related
|
||||
column in the CSV output since it has nothing to display there.
|
||||
|
||||
New in spot 2.2.2 (2016-12-16)
|
||||
|
||||
Build:
|
||||
|
|
|
|||
|
|
@ -497,6 +497,8 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
++arg;
|
||||
}
|
||||
products = to_pos_int(arg);
|
||||
if (products == 0)
|
||||
products_avg = false;
|
||||
break;
|
||||
case OPT_NOCHECKS:
|
||||
no_checks = true;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
# Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -217,3 +217,8 @@ diff foo expected
|
|||
|
||||
# This command used to crash. Report from František Blahoudek.
|
||||
run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba'
|
||||
|
||||
# The CSV file should not talk about product if --products=0
|
||||
ltlcross --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv
|
||||
grep product out.csv && exit 1
|
||||
check_csv out.csv
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue