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

ltlgrind: fix two bugs related to PSL formulas

Browse source 
* src/ltlvisit/mutation.cc: Do not bindly rewrite e[]->f and
e<>->f as e, since e is not a valid PSL formula.  Use !{e}
and {e} instead.  Also fix a memory leak in the handling of
bunops, discovered while testing the previous change.
* src/tests/ltlgrind.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2015-05-11 23:55:28 +02:00
parent 011a56846f
commit f55211336e
2 changed files with 52 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

55
src/ltlvisit/mutation.cc
View file

@ -122,14 +122,25 @@ namespace spot
const formula* first = bo->first();
const formula* second = bo->second();
result_ = 0;
auto op = bo->op();
bool left_is_sere = op == binop::EConcat
|| op == binop::EConcatMarked
|| op == binop::UConcat;
if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0)
result_ = first->clone();
{
if (!left_is_sere)
result_ = first->clone();
else if (op == binop::UConcat)
result_ = unop::instance(unop::NegClosure, first->clone());
else // EConcat or EConcatMarked
result_ = unop::instance(unop::Closure, first->clone());
}
if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0)
result_ = second->clone();
if (opts_ & Mut_Rewrite_Ops)
{
switch (bo->op())
switch (op)
{
case binop::U:
if (mutation_counter_-- == 0)
@ -155,7 +166,7 @@ namespace spot
}
if (opts_ & Mut_Split_Ops)
{
switch (bo->op())
switch (op)
{
case binop::Equiv:
if (mutation_counter_-- == 0)
@ -198,7 +209,7 @@ namespace spot
// instance() is incorrect, because each compiler
// could decide of a different order.
auto right = recurse(second);
result_ = binop::instance(bo->op(), recurse(first), right);
result_ = binop::instance(op, recurse(first), right);
}
}
}
@ -206,24 +217,29 @@ namespace spot
void visit(const bunop* bu)
{
const formula* c = bu->child()->clone();
result_ = 0;
result_ = nullptr;
auto op = bu->op();
if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0)
result_ = c->clone();
result_ = c;
if (opts_ & Mut_Simplify_Bounds)
{
if (bu->min() > 0 && mutation_counter_-- == 0)
result_ =
bunop::instance(bu->op(), c, bu->min() - 1, bu->max());
if (bu->min() > 0 && mutation_counter_-- == 0)
result_ = bunop::instance(bu->op(), c, 0, bu->max());
if (bu->max() != bunop::unbounded && bu->max() > bu->min()
&& mutation_counter_-- == 0)
result_ =
bunop::instance(bu->op(), c, bu->min(), bu->max() - 1);
if (bu->max() != bunop::unbounded && mutation_counter_-- == 0)
result_ = bunop::instance(bu->op(), c, bu->min(),
bunop::unbounded);
auto min = bu->min();
auto max = bu->max();
if (min > 0)
{
if (mutation_counter_-- == 0)
result_ = bunop::instance(op, c, min - 1, max);
if (mutation_counter_-- == 0)
result_ = bunop::instance(op, c, 0, max);
}
if (max != bunop::unbounded)
{
if (max > min && mutation_counter_-- == 0)
result_ = bunop::instance(op, c, min, max - 1);
if (mutation_counter_-- == 0)
result_ = bunop::instance(op, c, min, bunop::unbounded);
}
}
if (!result_)
{
@ -231,8 +247,7 @@ namespace spot
if (mutation_counter_ < 0)
result_ = bu->clone();
else
result_ = bunop::instance(bu->op(), recurse(c), bu->min(),
bu->max());
result_ = bunop::instance(op, recurse(c), bu->min(), bu->max());
}
}

18
src/tests/ltlgrind.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014 Laboratoire de Recherche et Dévelopement to
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Dévelopement to
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -26,6 +26,8 @@ checkopt()
{
cat >exp
run 0 ../../bin/ltlgrind "$@" > out
# The result must be parsable
../../bin/ltlfilt out
diff exp out
}
@ -165,3 +167,17 @@ p3 & p4
1 U (p3 & !p4)
1 U (!p3 & p4)
EOF
checkopt -f 'F({{p2;p0}[:*]}[]-> Xp0)' <<EOF
1
{{p2;p0}[:*]}[]-> Xp0
F!{{p2;p0}[:*]}
FXp0
F({{p2;p0}[:*]}[]-> p0)
F({{p2;p0}[:*]}[]-> 0)
F({p2;p0}[]-> Xp0)
F({{1;p0}[:*]}[]-> Xp0)
F({{p2;1}[:*]}[]-> Xp0)
F({p0[*2][:*]}[]-> Xp0)
F({p2[*2][:*]}[]-> Xp2)
EOF