You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
957 lines
22 KiB
957 lines
22 KiB
/* Written by Denis Oddoux, LIAFA, France *
|
|
* Copyright (c) 2001 Denis Oddoux *
|
|
* Modified by Paul Gastin, LSV, France *
|
|
* Copyright (c) 2007 Paul Gastin *
|
|
* Ported by Carlos Bederian, FaMAF, Argentina *
|
|
* Copyright (c) 2007 Carlos Bederian *
|
|
* *
|
|
* This program is free software; you can redistribute it and/or modify *
|
|
* it under the terms of the GNU General Public License as published by *
|
|
* the Free Software Foundation; either version 2 of the License, or *
|
|
* (at your option) any later version. *
|
|
* *
|
|
* This program is distributed in the hope that it will be useful, *
|
|
* but WITHOUT ANY WARRANTY; without even the implied warranty of *
|
|
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *
|
|
* GNU General Public License for more details. *
|
|
* *
|
|
* You should have received a copy of the GNU General Public License *
|
|
* along with this program; if not, write to the Free Software *
|
|
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*
|
|
* *
|
|
* Based on the translation algorithm by Gastin and Oddoux, *
|
|
* presented at the 13th International Conference on Computer Aided *
|
|
* Verification, CAV 2001, Paris, France. *
|
|
* Proceedings - LNCS 2102, pp. 53-65 *
|
|
* */
|
|
|
|
package jltl2ba;
|
|
|
|
import jltl2dstar.APMonom;
|
|
import jltl2dstar.NBA;
|
|
import prism.PrismException;
|
|
|
|
public class SimpleLTL {
|
|
|
|
public enum LTLType {
|
|
FALSE, TRUE,
|
|
AP,
|
|
NOT, NEXT,
|
|
OR, AND, EQUIV, IMPLIES,
|
|
UNTIL, RELEASE,
|
|
GLOBALLY, FINALLY
|
|
};
|
|
|
|
public SimpleLTL left;
|
|
public SimpleLTL right;
|
|
public LTLType kind;
|
|
public String ap;
|
|
|
|
public SimpleLTL(boolean v)
|
|
{
|
|
left = null;
|
|
right = null;
|
|
kind = v ? LTLType.TRUE : LTLType.FALSE;
|
|
ap = null;
|
|
}
|
|
|
|
public SimpleLTL(String prop)
|
|
{
|
|
left = null;
|
|
right = null;
|
|
kind = LTLType.AP;
|
|
ap = prop;
|
|
}
|
|
|
|
public SimpleLTL(LTLType type, SimpleLTL lft)
|
|
{
|
|
switch (type) {
|
|
case NOT:
|
|
case NEXT:
|
|
case GLOBALLY:
|
|
case FINALLY:
|
|
left = lft;
|
|
right = null;
|
|
kind = type;
|
|
ap = null;
|
|
break;
|
|
default:
|
|
// throw new PrismException("Trying to build invalid SimpleLTL");
|
|
}
|
|
}
|
|
|
|
public SimpleLTL(LTLType type, SimpleLTL lft, SimpleLTL rgt)
|
|
{
|
|
switch (type) {
|
|
case AND:
|
|
case OR:
|
|
case IMPLIES:
|
|
case EQUIV:
|
|
case UNTIL:
|
|
case RELEASE:
|
|
left = lft;
|
|
right = rgt;
|
|
kind = type;
|
|
ap = null;
|
|
break;
|
|
default:
|
|
// throw new PrismException("Trying to build invalid SimpleLTL");
|
|
}
|
|
}
|
|
|
|
public SimpleLTL(LTLType type, SimpleLTL lft, SimpleLTL rgt, String prop)
|
|
{
|
|
kind = type;
|
|
left = lft;
|
|
right = rgt;
|
|
ap = null;
|
|
if (prop != null) { ap = prop; }
|
|
}
|
|
|
|
public boolean equals(Object o)
|
|
{
|
|
if (o instanceof SimpleLTL) {
|
|
SimpleLTL other = (SimpleLTL) o;
|
|
if (kind == other.kind) {
|
|
switch (kind) {
|
|
case FALSE:case TRUE:
|
|
return true;
|
|
case NOT:case NEXT:case GLOBALLY:case FINALLY:
|
|
return left.equals(other.left);
|
|
case OR:case AND:case EQUIV:case IMPLIES:case UNTIL:case RELEASE:
|
|
return (left.equals(other.left) && right.equals(other.right));
|
|
case AP:
|
|
return ap.equals(other.ap);
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
else return false;
|
|
}
|
|
else return false;
|
|
}
|
|
|
|
public APSet getAPs()
|
|
{
|
|
APSet rv;
|
|
|
|
switch (kind) {
|
|
case NOT:case NEXT:
|
|
case GLOBALLY:case FINALLY:
|
|
rv = left.getAPs();
|
|
break;
|
|
case OR:case AND:
|
|
case EQUIV:case IMPLIES:
|
|
case UNTIL:case RELEASE:
|
|
rv = left.getAPs();
|
|
for (String s : right.getAPs())
|
|
rv.addAP(s);
|
|
break;
|
|
// terminals
|
|
case FALSE:case TRUE:
|
|
rv = new APSet();
|
|
break;
|
|
case AP:
|
|
rv = new APSet();
|
|
rv.addAP(ap);
|
|
break;
|
|
default:
|
|
rv = new APSet();
|
|
break;
|
|
}
|
|
return rv;
|
|
}
|
|
|
|
public SimpleLTL clone()
|
|
{
|
|
SimpleLTL rv = new SimpleLTL(kind,
|
|
left != null ? left.clone() : null,
|
|
right != null ? right.clone() : null,
|
|
ap);
|
|
return rv;
|
|
}
|
|
|
|
private boolean implies(SimpleLTL b)
|
|
{
|
|
return
|
|
(this.equals(b) ||
|
|
b.kind == LTLType.TRUE ||
|
|
kind == LTLType.FALSE ||
|
|
(b.kind == LTLType.AND && this.implies(b.left) && this.implies(b.right)) ||
|
|
(kind == LTLType.OR && left.implies(b) && right.implies(b)) ||
|
|
(kind == LTLType.AND && (left.implies(b) || right.implies(b))) ||
|
|
(b.kind == LTLType.OR && (this.implies(b.left) || this.implies(b.right))) ||
|
|
(b.kind == LTLType.UNTIL && this.implies(b.right)) ||
|
|
(kind == LTLType.RELEASE && right.implies(b)) ||
|
|
(kind == LTLType.UNTIL && left.implies(b) && right.implies(b)) ||
|
|
(b.kind == LTLType.RELEASE && this.implies(b.left) && this.implies(b.right)) ||
|
|
((kind == LTLType.UNTIL || kind == LTLType.RELEASE) && kind == b.kind &&
|
|
left.implies(b.left) && right.implies(b.right)));
|
|
}
|
|
|
|
// simplified PNF form
|
|
public SimpleLTL simplify()
|
|
{
|
|
SimpleLTL tmp, tmp2, a, b;
|
|
SimpleLTL rv = this;
|
|
|
|
switch (kind) {
|
|
case NOT:
|
|
tmp = this.pushNegation();
|
|
if (tmp.kind != LTLType.NOT)
|
|
rv = tmp.simplify();
|
|
else rv = tmp;
|
|
break;
|
|
case FINALLY:
|
|
left = left.simplify();
|
|
if (left.kind == LTLType.TRUE || left.kind == LTLType.FALSE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
else if (left.kind == LTLType.UNTIL) {
|
|
if (left.left.kind == LTLType.TRUE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
left = left.right;
|
|
/* fall thru */
|
|
}
|
|
tmp = new SimpleLTL(LTLType.UNTIL, new SimpleLTL(true), left);
|
|
rv = tmp.simplify();
|
|
break;
|
|
|
|
case GLOBALLY:
|
|
left = left.simplify();
|
|
if (left.kind == LTLType.FALSE || left.kind == LTLType.TRUE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
else if (left.kind == LTLType.RELEASE) {
|
|
if (left.left.kind == LTLType.FALSE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
left = left.right; /* [] (p V q) = [] q */
|
|
/* fall thru */
|
|
}
|
|
tmp = new SimpleLTL(LTLType.RELEASE, new SimpleLTL(false), left);
|
|
rv = tmp.simplify();
|
|
break;
|
|
|
|
case UNTIL:
|
|
left = left.simplify();
|
|
right = right.simplify();
|
|
|
|
if (right.kind == LTLType.TRUE
|
|
|| right.kind == LTLType.FALSE
|
|
|| left.kind == LTLType.FALSE) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
if (left.implies(right)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
/* (p U q) U p = (q U p) */
|
|
if (left.kind == LTLType.UNTIL && left.left.equals(right)) {
|
|
left = left.right;
|
|
break;
|
|
}
|
|
if (right.kind == LTLType.UNTIL && left.implies(right.left)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
/* X p U X q == X (p U q) */
|
|
if (right.kind == LTLType.NEXT && left.kind == LTLType.NEXT) {
|
|
rv = new SimpleLTL(LTLType.NEXT,
|
|
new SimpleLTL(LTLType.UNTIL, left.left, right.left));
|
|
break;
|
|
}
|
|
|
|
/* F X p == X F p */
|
|
if (left.kind == LTLType.TRUE && right.kind == LTLType.NEXT) {
|
|
rv = new SimpleLTL(LTLType.NEXT,
|
|
new SimpleLTL(LTLType.UNTIL, new SimpleLTL(true), right.left));
|
|
break;
|
|
}
|
|
|
|
/* F G F p == G F p */
|
|
if (left.kind == LTLType.TRUE &&
|
|
right.kind == LTLType.RELEASE &&
|
|
right.left.kind == LTLType.FALSE &&
|
|
right.right.kind == LTLType.UNTIL &&
|
|
right.right.left.kind == LTLType.TRUE) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
if (left.kind != LTLType.TRUE) {
|
|
tmp = new SimpleLTL(LTLType.NOT, right.clone());
|
|
if (tmp.pushNegation().implies(left))
|
|
left = new SimpleLTL(true);
|
|
break;
|
|
}
|
|
break;
|
|
|
|
case RELEASE:
|
|
left = left.simplify();
|
|
right = right.simplify();
|
|
|
|
if (right.kind == LTLType.FALSE
|
|
|| right.kind == LTLType.TRUE
|
|
|| left.kind == LTLType.TRUE) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
/* p V p = p */
|
|
if (right.implies(left)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
/* F V (p V q) == F V q */
|
|
if (left.kind == LTLType.FALSE && right.kind == LTLType.RELEASE) {
|
|
right = right.right;
|
|
break;
|
|
}
|
|
|
|
/* G X p == X G p */
|
|
if (left.kind == LTLType.FALSE && right.kind == LTLType.NEXT) {
|
|
rv = new SimpleLTL(LTLType.NEXT,
|
|
new SimpleLTL(LTLType.RELEASE,
|
|
new SimpleLTL(false), right.left));
|
|
break;
|
|
}
|
|
/* G F G p == F G p */
|
|
if (left.kind == LTLType.FALSE &&
|
|
right.kind == LTLType.UNTIL &&
|
|
right.left.kind == LTLType.TRUE &&
|
|
right.right.kind == LTLType.RELEASE &&
|
|
right.right.left.kind == LTLType.FALSE) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
if (right.kind == LTLType.RELEASE
|
|
&& right.left.implies(left)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
if (left.kind != LTLType.FALSE) {
|
|
tmp = new SimpleLTL(LTLType.NOT, right.clone());
|
|
if (left.implies(tmp.pushNegation()))
|
|
left = new SimpleLTL(false);
|
|
break;
|
|
}
|
|
break;
|
|
|
|
case NEXT:
|
|
left = left.simplify();
|
|
|
|
if (left.kind == LTLType.TRUE || left.kind == LTLType.FALSE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
|
|
/* X G F p == G F p */
|
|
if (left.kind == LTLType.RELEASE &&
|
|
left.left.kind == LTLType.FALSE &&
|
|
left.right.kind == LTLType.UNTIL &&
|
|
left.right.left.kind == LTLType.TRUE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
/* X F G p == F G p */
|
|
if (left.kind == LTLType.UNTIL &&
|
|
left.left.kind == LTLType.TRUE &&
|
|
left.right.kind == LTLType.RELEASE &&
|
|
left.right.left.kind == LTLType.FALSE) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
break;
|
|
case IMPLIES:
|
|
left = left.simplify();
|
|
right = right.simplify();
|
|
|
|
if (left.implies(right)) {
|
|
rv = new SimpleLTL(true);
|
|
break;
|
|
}
|
|
|
|
tmp = new SimpleLTL(LTLType.NOT, left);
|
|
tmp = new SimpleLTL(LTLType.OR, tmp.pushNegation(), right);
|
|
rv = tmp.rewrite();
|
|
break;
|
|
|
|
case EQUIV:
|
|
left = left.simplify();
|
|
right = right.simplify();
|
|
|
|
if (left.implies(right) &&
|
|
right.implies(left)) {
|
|
rv = new SimpleLTL(true);
|
|
break;
|
|
}
|
|
|
|
a = new SimpleLTL(LTLType.AND, left.clone(), right.clone());
|
|
tmp = new SimpleLTL(LTLType.NOT, left);
|
|
tmp2 = new SimpleLTL(LTLType.NOT, right);
|
|
b = new SimpleLTL(LTLType.AND, tmp.pushNegation(), tmp2.pushNegation());
|
|
rv = new SimpleLTL(LTLType.OR, a.rewrite(), b.rewrite());
|
|
rv = rv.rewrite();
|
|
break;
|
|
|
|
case AND:
|
|
left = left.simplify();
|
|
right = right.simplify();
|
|
|
|
/* p && (q U p) = p */
|
|
if (right.kind == LTLType.UNTIL
|
|
&& right.right.equals(left)) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
if (left.kind == LTLType.UNTIL
|
|
&& left.right.equals(right)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
/* p && (q V p) == q V p */
|
|
if (right.kind == LTLType.RELEASE
|
|
&& right.right.equals(left)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
if (left.kind == LTLType.RELEASE
|
|
&& left.right.equals(right)) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
|
|
/* (p U q) && (r U q) = (p && r) U q */
|
|
if (right.kind == LTLType.UNTIL
|
|
&& left.kind == LTLType.UNTIL
|
|
&& right.right.equals(left.right)) {
|
|
rv = new SimpleLTL(LTLType.UNTIL,
|
|
new SimpleLTL(LTLType.AND, left.left, right.left),
|
|
left.right);
|
|
break;
|
|
}
|
|
|
|
/* (p V q) && (p V r) = p V (q && r) */
|
|
if (right.kind == LTLType.RELEASE
|
|
&& left.kind == LTLType.RELEASE
|
|
&& right.left.equals(left.left)) {
|
|
rv = new SimpleLTL(LTLType.RELEASE,
|
|
right.left,
|
|
new SimpleLTL(LTLType.AND, left.right, right.right));
|
|
break;
|
|
}
|
|
|
|
/* X p && X q == X (p && q) */
|
|
if (right.kind == LTLType.NEXT && left.kind == LTLType.NEXT) {
|
|
rv = new SimpleLTL(LTLType.NEXT,
|
|
new SimpleLTL(LTLType.AND, right.left, left.left));
|
|
break;
|
|
}
|
|
|
|
/* (p V q) && (r U q) == p V q */
|
|
if (right.kind == LTLType.UNTIL
|
|
&& left.kind == LTLType.RELEASE
|
|
&& left.right.equals(right.right)) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
|
|
if (left.equals(right) /* (p && p) == p */
|
|
||right.kind == LTLType.FALSE /* (p && F) == F */
|
|
|| left.kind == LTLType.TRUE /* (T && p) == p */
|
|
|| right.implies(left)) { /* NEW */
|
|
rv = right;
|
|
break;
|
|
}
|
|
if (right.kind == LTLType.TRUE /* (p && T) == p */
|
|
|| left.kind == LTLType.FALSE /* (F && p) == F */
|
|
|| left.implies(right)) { /* NEW */
|
|
rv = left;
|
|
break;
|
|
}
|
|
|
|
/* F G p && F G q == F G (p && q) */
|
|
if (left.kind == LTLType.UNTIL &&
|
|
left.left.kind == LTLType.TRUE &&
|
|
left.right.kind == LTLType.RELEASE &&
|
|
left.right.left.kind == LTLType.FALSE &&
|
|
right.kind == LTLType.UNTIL &&
|
|
right.left.kind == LTLType.TRUE &&
|
|
right.right.kind == LTLType.RELEASE &&
|
|
right.right.left.kind == LTLType.FALSE) {
|
|
rv = new SimpleLTL(LTLType.UNTIL,
|
|
new SimpleLTL(true),
|
|
new SimpleLTL(LTLType.RELEASE,
|
|
new SimpleLTL(false),
|
|
new SimpleLTL(LTLType.AND,
|
|
left.right.right,
|
|
right.right.right)));
|
|
break;
|
|
}
|
|
|
|
tmp = new SimpleLTL(LTLType.NOT, right.clone());
|
|
if (left.implies(tmp.pushNegation())) {
|
|
rv = new SimpleLTL(false);
|
|
break;
|
|
}
|
|
tmp = new SimpleLTL(LTLType.NOT, left.clone());
|
|
if (right.implies(tmp.pushNegation())) {
|
|
rv = new SimpleLTL(false);
|
|
break;
|
|
}
|
|
break;
|
|
|
|
case OR:
|
|
left = left.simplify();
|
|
right = right.simplify();
|
|
|
|
/* p || (q U p) == q U p */
|
|
if (right.kind == LTLType.UNTIL
|
|
&& right.right.equals(left)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
/* p || (q V p) == p */
|
|
if (right.kind == LTLType.RELEASE
|
|
&& right.right.equals(left)) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
|
|
/* (p U q) || (p U r) = p U (q || r) */
|
|
if (right.kind == LTLType.UNTIL
|
|
&& left.kind == LTLType.UNTIL
|
|
&& right.left.equals(left.left)) {
|
|
rv = new SimpleLTL(LTLType.UNTIL,
|
|
right.left,
|
|
new SimpleLTL(LTLType.OR, left.right, right.right));
|
|
break;
|
|
}
|
|
|
|
if (left.equals(right) /* (p || p) == p */
|
|
||right.kind == LTLType.FALSE /* (p || F) == p */
|
|
|| left.kind == LTLType.TRUE /* (T || p) == T */
|
|
|| right.implies(left)) {
|
|
rv = left;
|
|
break;
|
|
}
|
|
if (right.kind == LTLType.TRUE /* (p || T) == T */
|
|
|| left.kind == LTLType.FALSE /* (F || p) == p */
|
|
|| left.implies(right)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
/* (p V q) || (r V q) = (p || r) V q */
|
|
if (right.kind == LTLType.RELEASE
|
|
&& left.kind == LTLType.RELEASE
|
|
&& left.right.equals(right.right)) {
|
|
rv = new SimpleLTL(LTLType.RELEASE,
|
|
new SimpleLTL(LTLType.OR, left.left, right.left),
|
|
right.right);
|
|
break;
|
|
}
|
|
|
|
/* (p V q) || (r U q) == r U q */
|
|
if (right.kind == LTLType.UNTIL
|
|
&& left.kind == LTLType.RELEASE
|
|
&& left.right.equals(right.right)) {
|
|
rv = right;
|
|
break;
|
|
}
|
|
|
|
/* G F p || G F q == G F (p || q) */
|
|
if (left.kind == LTLType.RELEASE &&
|
|
left.left.kind == LTLType.FALSE &&
|
|
left.right.kind == LTLType.UNTIL &&
|
|
left.right.left.kind == LTLType.TRUE &&
|
|
right.kind == LTLType.RELEASE &&
|
|
right.left.kind == LTLType.FALSE &&
|
|
right.right.kind == LTLType.UNTIL &&
|
|
right.right.left.kind == LTLType.TRUE) {
|
|
rv = new SimpleLTL(LTLType.RELEASE,
|
|
new SimpleLTL(false),
|
|
new SimpleLTL(LTLType.UNTIL,
|
|
new SimpleLTL(true),
|
|
new SimpleLTL(LTLType.OR,left.right.right,right.right.right)));
|
|
break;
|
|
}
|
|
|
|
tmp = new SimpleLTL(LTLType.NOT, right.clone());
|
|
if (tmp.pushNegation().implies(left)) {
|
|
rv = new SimpleLTL(true);
|
|
break;
|
|
}
|
|
tmp = new SimpleLTL(LTLType.NOT, left.clone());
|
|
if (tmp.pushNegation().implies(right)) {
|
|
rv = new SimpleLTL(true);
|
|
break;
|
|
}
|
|
break;
|
|
}
|
|
return rv;
|
|
}
|
|
|
|
public SimpleLTL negate() {
|
|
return new SimpleLTL(LTLType.NOT, this);
|
|
}
|
|
|
|
public SimpleLTL pushNegation()
|
|
{
|
|
SimpleLTL m;
|
|
boolean pushBothOperands = false;
|
|
|
|
if (kind != LTLType.NOT)
|
|
return this;
|
|
// throw new PrismException("No NOT to push!");
|
|
|
|
switch (left.kind) {
|
|
case TRUE:
|
|
left = null;
|
|
kind = LTLType.FALSE;
|
|
break;
|
|
case FALSE:
|
|
left = null;
|
|
kind = LTLType.TRUE;
|
|
break;
|
|
case NOT:
|
|
m = left.left;
|
|
left = m.left;
|
|
right = m.right;
|
|
kind = m.kind;
|
|
if (kind == LTLType.AP) { ap = m.ap; }
|
|
break;
|
|
case RELEASE:
|
|
kind = LTLType.UNTIL;
|
|
pushBothOperands = true;
|
|
break;
|
|
case UNTIL:
|
|
kind = LTLType.RELEASE;
|
|
pushBothOperands = true;
|
|
break;
|
|
case NEXT:
|
|
kind = LTLType.NEXT;
|
|
left.kind = LTLType.NOT;
|
|
left = left.pushNegation();
|
|
break;
|
|
case AND:
|
|
kind = LTLType.OR;
|
|
pushBothOperands = true;
|
|
break;
|
|
case OR:
|
|
kind = LTLType.AND;
|
|
pushBothOperands = true;
|
|
break;
|
|
case FINALLY:
|
|
kind = LTLType.GLOBALLY;
|
|
left.kind = LTLType.NOT;
|
|
left = left.pushNegation();
|
|
break;
|
|
case GLOBALLY:
|
|
kind = LTLType.FINALLY;
|
|
left.kind = LTLType.NOT;
|
|
left = left.pushNegation();
|
|
break;
|
|
case AP:
|
|
return this;
|
|
}
|
|
if (pushBothOperands) {
|
|
m = new SimpleLTL(LTLType.NOT, left.right);
|
|
right = m.pushNegation();
|
|
left.kind = LTLType.NOT;
|
|
left.right = null;
|
|
left = left.pushNegation();
|
|
}
|
|
return this.rewrite();
|
|
}
|
|
|
|
public SimpleLTL rewrite()
|
|
{
|
|
return this.rightLinked().canonical();
|
|
}
|
|
|
|
public SimpleLTL rightLinked()
|
|
{
|
|
SimpleLTL tmp;
|
|
SimpleLTL n = this;
|
|
|
|
if (n.kind == LTLType.AND || n.kind == LTLType.OR) {
|
|
while (n.left != null && n.left.kind == n.kind) {
|
|
tmp = n.left;
|
|
n.left = tmp.right;
|
|
tmp.right = n;
|
|
n = tmp;
|
|
}
|
|
}
|
|
if (n.left != null)
|
|
n.left = n.left.rightLinked();
|
|
if (n.right != null)
|
|
n.right = n.right.rightLinked();
|
|
|
|
return n;
|
|
}
|
|
|
|
public SimpleLTL canonical()
|
|
{
|
|
return this; // No caches here, yet
|
|
|
|
/* SimpleLTL m; // assumes input is right_linked
|
|
|
|
if ((m = in_cache(n)) != ZN)
|
|
return m;
|
|
|
|
n->rgt = canonical(n->rgt);
|
|
n->lft = canonical(n->lft);
|
|
|
|
return cached(n);
|
|
*/
|
|
}
|
|
|
|
public int countNodes()
|
|
{
|
|
switch (kind) {
|
|
case AND:
|
|
case OR:
|
|
case IMPLIES:
|
|
case EQUIV:
|
|
case UNTIL:
|
|
case RELEASE:
|
|
return left.countNodes() + right.countNodes() + 1;
|
|
case NEXT:
|
|
case FINALLY:
|
|
case GLOBALLY:
|
|
case NOT:
|
|
return left.countNodes() + 1;
|
|
default:
|
|
return 1;
|
|
}
|
|
}
|
|
|
|
public int countPredicates()
|
|
{
|
|
switch (kind) {
|
|
case AND:
|
|
case OR:
|
|
case IMPLIES:
|
|
case EQUIV:
|
|
case UNTIL:
|
|
case RELEASE:
|
|
return left.countPredicates() + right.countPredicates();
|
|
case NEXT:
|
|
case FINALLY:
|
|
case GLOBALLY:
|
|
case NOT:
|
|
return left.countPredicates();
|
|
case AP:
|
|
return 1;
|
|
default:
|
|
return 0;
|
|
}
|
|
}
|
|
|
|
public String toString()
|
|
{
|
|
String rv = "";
|
|
|
|
switch (kind) {
|
|
case OR:
|
|
rv = "(" + left.toString() + " || " + right.toString() + ")";
|
|
break;
|
|
case AND:
|
|
rv = "(" + left.toString() + " && " + right.toString() + ")";
|
|
break;
|
|
case UNTIL:
|
|
rv = "(" + left.toString() + " U " + right.toString() + ")";
|
|
break;
|
|
case RELEASE:
|
|
rv = "(" + left.toString() + " V " + right.toString() + ")";
|
|
break;
|
|
case IMPLIES:
|
|
rv = "(" + left.toString() + " -> " + right.toString() + ")";
|
|
break;
|
|
case EQUIV:
|
|
rv = "(" + left.toString() + " <-> " + right.toString() + ")";
|
|
break;
|
|
case NEXT:
|
|
rv = "X " + left.toString();
|
|
break;
|
|
case FINALLY:
|
|
rv = "F " + left.toString();
|
|
break;
|
|
case GLOBALLY:
|
|
rv = "G " + left.toString();
|
|
break;
|
|
case NOT:
|
|
rv = "! " + left.toString();
|
|
break;
|
|
case FALSE:
|
|
rv = "false";
|
|
break;
|
|
case TRUE:
|
|
rv = "true";
|
|
break;
|
|
case AP:
|
|
rv = ap;
|
|
break;
|
|
default:
|
|
rv = null;
|
|
}
|
|
return rv;
|
|
}
|
|
|
|
// ltl2dstar stuff
|
|
public boolean isCoSafe()
|
|
{
|
|
switch(kind) {
|
|
case RELEASE:
|
|
case GLOBALLY:
|
|
return false;
|
|
default:
|
|
if (left != null && !left.isCoSafe()) {
|
|
return false;
|
|
}
|
|
if (right != null && !right.isCoSafe()) {
|
|
return false;
|
|
}
|
|
return true;
|
|
}
|
|
}
|
|
|
|
public boolean hasNextStep()
|
|
{
|
|
if (kind == LTLType.NEXT) {
|
|
return true;
|
|
}
|
|
if (left != null && left.hasNextStep()) {
|
|
return true;
|
|
}
|
|
if (right != null && right.hasNextStep()) {
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
public SimpleLTL toDNF() throws PrismException
|
|
{
|
|
switch (kind) {
|
|
case TRUE:
|
|
return new SimpleLTL(true);
|
|
case FALSE:
|
|
return new SimpleLTL(false);
|
|
case NOT:
|
|
return new SimpleLTL(LTLType.NOT, left.toDNF());
|
|
case AP:
|
|
return new SimpleLTL(ap);
|
|
case OR:
|
|
return new SimpleLTL(LTLType.OR, left.toDNF(), right.toDNF());
|
|
case AND:
|
|
SimpleLTL l = left.toDNF();
|
|
SimpleLTL r = right.toDNF();
|
|
|
|
if (l.kind == LTLType.OR) {
|
|
SimpleLTL a, b;
|
|
a = l.left;
|
|
b = l.right;
|
|
|
|
if (r.kind == LTLType.OR) {
|
|
SimpleLTL c, d;
|
|
c=r.left;
|
|
d=r.right;
|
|
|
|
SimpleLTL a_c = new SimpleLTL(LTLType.AND, a, c);
|
|
SimpleLTL b_c = new SimpleLTL(LTLType.AND, b, c);
|
|
SimpleLTL a_d = new SimpleLTL(LTLType.AND, a, d);
|
|
SimpleLTL b_d = new SimpleLTL(LTLType.AND, b, d);
|
|
|
|
return new SimpleLTL(LTLType.OR,
|
|
(new SimpleLTL(LTLType.OR, a_c, b_c)).toDNF(),
|
|
(new SimpleLTL(LTLType.OR, a_d, b_d)).toDNF());
|
|
} else {
|
|
SimpleLTL a_c = new SimpleLTL(LTLType.AND, a, r);
|
|
SimpleLTL b_c = new SimpleLTL(LTLType.AND, b, r);
|
|
|
|
return new SimpleLTL(LTLType.OR, a_c.toDNF(), b_c.toDNF());
|
|
}
|
|
} else if (r.kind == LTLType.OR) {
|
|
SimpleLTL a, b;
|
|
a = r.left;
|
|
b = r.right;
|
|
|
|
SimpleLTL a_c = new SimpleLTL(LTLType.AND, l, a);
|
|
SimpleLTL b_c = new SimpleLTL(LTLType.AND, l, b);
|
|
|
|
return new SimpleLTL(LTLType.OR, a_c.toDNF(), b_c.toDNF());
|
|
} else {
|
|
return new SimpleLTL(LTLType.AND, l, r);
|
|
}
|
|
default:
|
|
throw new PrismException("Illegal operator for DNF!");
|
|
}
|
|
}
|
|
|
|
/** Returns an APMonom representing the formula rooted at
|
|
* this node. Formula has to be in DNF. */
|
|
public APMonom toMonom(APSet apset) throws PrismException
|
|
{
|
|
APMonom result = new APMonom(true);
|
|
|
|
switch (kind) {
|
|
case AND: {
|
|
APMonom l = left.toMonom(apset);
|
|
APMonom r = right.toMonom(apset);
|
|
|
|
result = l.and(r);
|
|
return result;
|
|
}
|
|
case NOT:
|
|
switch (left.kind) {
|
|
case AP:
|
|
result.setValue(apset.indexOf(left.ap), false);
|
|
return result;
|
|
case FALSE:
|
|
return new APMonom(true);
|
|
case TRUE:
|
|
return new APMonom(false);
|
|
default:
|
|
throw new PrismException("Formula not in DNF!");
|
|
}
|
|
case AP:
|
|
result.setValue(apset.indexOf(ap), true);
|
|
return result;
|
|
case FALSE:
|
|
return new APMonom(false);
|
|
case TRUE:
|
|
return new APMonom(true);
|
|
default:
|
|
throw new PrismException("Formula not in DNF!");
|
|
}
|
|
}
|
|
|
|
public NBA toNBA(APSet apset) throws PrismException
|
|
{
|
|
Alternating a = new Alternating(this, apset);
|
|
// a.print(System.out);
|
|
Generalized g = new Generalized(a);
|
|
// g.print(System.out, apset);
|
|
Buchi b = new Buchi(g);
|
|
// b.print_spin(System.out, apset);
|
|
NBA nba = b.toNBA(apset);
|
|
// nba.print(System.out);
|
|
return nba;
|
|
}
|
|
|
|
public NBA toNBA() throws PrismException
|
|
{
|
|
return this.toNBA(new APSet());
|
|
}
|
|
}
|