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

Fix syntactic implication rule between R/M and U/W.

* doc/tl/tl.tex, src/ltlvisit/simplify.cc: Fix the rule.
* src/ltltest/reduccmp.test, src/ltltest/syntimpl.test:
Add more tests.
parent 70e3e2cd
......@@ -1735,9 +1735,9 @@ $f_U$ & & & $f_U\simp g$ &
\hline
$\X f$ & & $f\simp g_E$ & $f\simp g$ & & & & & & & & \\
\hline
$f_1\U f_2$ & \band{f_1}{g}{f_2}{g} & & & \band{f_1}{g_1}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & \bone{f_2}{g} & & & \\
$f_1\U f_2$ & \band{f_1}{g}{f_2}{g} & & & \band{f_1}{g_1}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_2}{f_2}{g_1}{f_2}{g_2} & \banD{f_1}{g_2}{f_2}{g_1}{f_2}{g_2} & \bone{f_2}{g} & & & \\
\hline
$f_1\W f_2$ & \band{f_1}{g}{f_2}{g} & & & \band{f_1}{g_2}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & & \band{f_1}{g}{f_2}{g} & & & \\
$f_1\W f_2$ & \band{f_1}{g}{f_2}{g} & & & \band{f_1}{g_2}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_2}{f_2}{g_1}{f_2}{g_2} & & \band{f_1}{g}{f_2}{g} & & & \\
\hline
$f_1\R f_2$ & \bone{f_2}{g} & & & & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_1}{f_2}{g_2} & \band{f_2}{g_1}{f_2}{g_2} & \bone{f_2}{g} & & & \\
\hline
......
......@@ -324,6 +324,7 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})'
run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc'
# not reduced
run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
......
#! /bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
......@@ -93,3 +94,8 @@ run 0 ../syntimpl 0 'a R b' 'a'
run 0 ../syntimpl 0 'p2' 'p3 || G(p2 && p5)'
run 0 ../syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'
run 0 ../syntimpl 0 'Xc W 0' 'Xc R b'
run 1 ../syntimpl 0 '(c&b) W (b&a)' 'a R b'
exit 0
\ No newline at end of file
......@@ -235,8 +235,16 @@ namespace spot
bool
implication(const formula* f1, const formula* f2)
{
return (options.synt_impl && syntactic_implication(f1, f2))
|| (options.containment_checks && contained(f1, f2));
trace << "[->] does " << to_string(f1) << " implies "
<< to_string(f2) << " ?" << std::endl;
if ((options.synt_impl && syntactic_implication(f1, f2))
|| (options.containment_checks && contained(f1, f2)))
{
trace << "[->] Yes" << std::endl;
return true;
}
trace << "[->] No" << std::endl;
return false;
}
// Return true if f1 => f2 syntactically
......@@ -3910,7 +3918,7 @@ namespace spot
else if ((fo == binop::U && (go == binop::R || go == binop::M))
|| (fo == binop::W && go == binop::R))
{
if (syntactic_implication(f1, g1)
if (syntactic_implication(f1, g2)
&& syntactic_implication(f2, g1)
&& syntactic_implication(f2, g2))
return true;
......
Supports Markdown
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