alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Fix genltl --gh-r

Browse source 
Reported by František Blahoudek.

* src/bin/genltl.cc (R_n): Really generate (GFp1 || FGp2), not
(GFp1 || GFp2).
* NEWS: Mention the bug.
* THANKS: Update.
This commit is contained in:
Alexandre Duret-Lutz 2013-04-30 00:01:35 +02:00
parent b881c10155
commit e2378b4904
3 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -1,6 +1,8 @@
New in spot 1.1a (not yet released): New in spot 1.1a (not yet released):
Nothing yet. Bug fixes:
- genltl --gh-r generated the wrong formulas due to a typo.
New in spot 1.1 (2013-04-28): New in spot 1.1 (2013-04-28):

1
THANKS
View file

@ -5,6 +5,7 @@ Akim Demaille
Christian Dax Christian Dax
Étienne Renault Étienne Renault
Felix Klaedtke Felix Klaedtke
František Blahoudek
Gerard J. Holzmann Gerard J. Holzmann
Heikki Tauriainen Heikki Tauriainen
Jean-Michel Couvreur Jean-Michel Couvreur

6
src/bin/genltl.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de // Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -429,7 +429,7 @@ R_n(std::string name, int n)
p << name << i + 1; p << name << i + 1;
pi = env.require(p.str()); pi = env.require(p.str());
const formula* fg = G_(F_(pi->clone())); const formula* fg = F_(G_(pi->clone()));
const formula* f = Or_(gf, fg); const formula* f = Or_(gf, fg);