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

neverparse: Fix parsing of Modella's neverclaims.

Reported by František Blahoudek.

* src/neverparse/neverclaimparse.yy: Fix.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention the fix.
parent a4934c4f
......@@ -3,6 +3,7 @@ New in spot 1.2.4a (not yet released)
* Bug fixes:
- Fix simplification of bounded repetition in SERE formulas.
- Fix parsing of neverclaims produced by Modella.
New in spot 1.2.4 (2014-05-15)
......
/* -*- coding: utf-8 -*-
** Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
** Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
**
** This file is part of Spot, a model checking library.
......@@ -191,7 +191,7 @@ transitions:
}
formula: FORMULA | "false" { $$ = new std::string("0"); }
formula: FORMULA | IDENT | "false" { $$ = new std::string("0"); }
opt_dest:
/* empty */
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -172,6 +172,40 @@ EOF
grep input: stderr >> stderrfilt
diff stderrfilt expected
# This output from MoDeLLa was not property parsed by Spot because of
# the missing parentheses around p0. Report from František Blahoudek.
cat >input <<EOF
never{
T0_init:
if
:: true -> goto T1
:: p0 -> goto T2
fi;
T1:
if
:: true -> goto T1
:: p0 -> goto accept_T3
fi;
T2:
if
:: p0 -> goto accept_T3
fi;
accept_T3:
if
:: p0 -> goto T2
fi;
}
EOF
cat >expected<<EOF
transitions: 6
states: 4
EOF
run 0 ../ltl2tgba -ks -XN input > output
diff output expected
cat >formulae<<EOF
a
FG a
......
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