s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Add partial support for multi-objective queries expressed as Boolean expressions. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10456 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
d44e1c7ecc
commit
795627c953
3 changed files with 488 additions and 5 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 384
      prism/src/parser/BooleanUtils.java
  2. 27
      prism/src/parser/ast/RelOp.java
  3. 82
      prism/src/prism/NondetModelChecker.java

384
prism/src/parser/BooleanUtils.java
View File

@ -0,0 +1,384 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
//
//------------------------------------------------------------------------------
//
// This file is part of PRISM.
//
// PRISM 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.
//
// PRISM 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 PRISM; if not, write to the Free Software Foundation,
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
//
//==============================================================================
package parser;
import java.io.ByteArrayInputStream;
import java.util.ArrayList;
import java.util.List;
import parser.ast.Expression;
import parser.ast.ExpressionBinaryOp;
import parser.ast.ExpressionLabel;
import parser.ast.ExpressionProb;
import parser.ast.ExpressionQuant;
import parser.ast.ExpressionReward;
import parser.ast.ExpressionUnaryOp;
import parser.visitor.ASTTraverseModify;
import prism.PrismException;
import prism.PrismLangException;
public class BooleanUtils
{
/**
* Extract the conjuncts from a conjunction in the form of zero or more nested
* binary conjunctions represented by ExpressionBinaryOp objects.
*
* @param expr The conjunction to extract from
* @param conjuncts The list to insert conjuncts into
*/
public static void extractConjuncts(Expression expr, List<Expression> conjuncts)
{
// Traverse depth-first, and add any non-ands to the list
if (Expression.isAnd(expr)) {
extractConjuncts(((ExpressionBinaryOp) expr).getOperand1(), conjuncts);
extractConjuncts(((ExpressionBinaryOp) expr).getOperand2(), conjuncts);
} else {
conjuncts.add(expr);
}
}
/**
* Extract the disjuncts from a disjunction in the form of zero or more nested
* binary disjunctions represented by ExpressionBinaryOp objects.
*
* @param expr The disjunction to extract from
* @param disjuncts The list to insert disjuncts into
*/
public static void extractDisjuncts(Expression expr, List<Expression> disjuncts)
{
// Traverse depth-first, and add any non-ors to the list
if (Expression.isAnd(expr)) {
extractDisjuncts(((ExpressionBinaryOp) expr).getOperand1(), disjuncts);
extractDisjuncts(((ExpressionBinaryOp) expr).getOperand2(), disjuncts);
} else {
disjuncts.add(expr);
}
}
/**
* Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and
* replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result
* is also returned. As an optimisation, expressions that results in true/false for all states are converted to an
* actual true/false, and duplicate results (or their negations) reuse the same label. BDDs giving the states which
* satisfy each label are put into the vector labelDDs, which should be empty when this function is called.
*/
public static Expression extractAtomsFromBooleanExpression(Expression expr, List<ExpressionQuant> labelDDs) throws PrismException
{
// A state formula
if (expr instanceof ExpressionProb || expr instanceof ExpressionReward) {
labelDDs.add((ExpressionQuant) expr);
return new ExpressionLabel("L" + (labelDDs.size() - 1));
}
// A path formula (recurse, modify, return)
else if (Expression.isOr(expr)) {
ExpressionBinaryOp exprOr = (ExpressionBinaryOp) expr;
exprOr.setOperand1(extractAtomsFromBooleanExpression(exprOr.getOperand1(), labelDDs));
exprOr.setOperand2(extractAtomsFromBooleanExpression(exprOr.getOperand2(), labelDDs));
} else if (Expression.isAnd(expr)) {
ExpressionBinaryOp exprAnd = (ExpressionBinaryOp) expr;
exprAnd.setOperand1(extractAtomsFromBooleanExpression(exprAnd.getOperand1(), labelDDs));
exprAnd.setOperand2(extractAtomsFromBooleanExpression(exprAnd.getOperand2(), labelDDs));
} else if (Expression.isImplies(expr)) {
ExpressionBinaryOp exprImplies = (ExpressionBinaryOp) expr;
exprImplies.setOperand1(extractAtomsFromBooleanExpression(exprImplies.getOperand1(), labelDDs));
exprImplies.setOperand2(extractAtomsFromBooleanExpression(exprImplies.getOperand2(), labelDDs));
} else if (Expression.isNot(expr)) {
ExpressionUnaryOp exprNot = (ExpressionUnaryOp) expr;
exprNot.setOperand(extractAtomsFromBooleanExpression(exprNot.getOperand(), labelDDs));
} else {
throw new PrismException("arg " + expr);
}
return expr;
}
/**
* Convert a Boolean expression to positive normal form,
* i.e., remove any instances of =>, <=> or () and then push
* all negation inwards so that it only occurs on "propositions".
* A "proposition" is any Expression object that
* is not an operator used to define a Boolean expression (!, &, |, =>, <=>, ()).
* The passed in expression is modified, and the result is returned.
*/
public static Expression convertToPositiveNormalForm(Expression expr) throws PrismLangException
{
// First expand implies/iff/parentheses
Expression exprBool = (Expression) expr.accept(new ASTTraverseModify() {
public Object visit(ExpressionUnaryOp e) throws PrismLangException
{
// Remove parentheses: (a)
if (Expression.isParenth(e)) {
Expression a = (Expression)(e.getOperand().accept(this));
// (a) == a
return a;
}
return super.visit(e);
}
public Object visit(ExpressionBinaryOp e) throws PrismLangException
{
// Remove implication: a => b
if (Expression.isImplies(e)) {
Expression a = (Expression)(e.getOperand1().accept(this));
Expression b = (Expression)(e.getOperand2().accept(this));
// a => b == !a | b
return Expression.Or(Expression.Not(a), b);
}
// Remove iff: a <=> b
if (Expression.isImplies(e)) {
Expression a = (Expression)(e.getOperand1().accept(this));
Expression b = (Expression)(e.getOperand2().accept(this));
// a <=> b == (a | !b) & (!a | b)
return Expression.And(Expression.Or(a, Expression.Not(b)), Expression.Or(Expression.Not(a.deepCopy()), b.deepCopy()));
}
return super.visit(e);
}
});
// Then do conversion to +ve normal form
return doConversionToPositiveNormalForm(exprBool);
}
/**
* Do the main part of the conversion of a Boolean expression to positive normal form,
* i.e., push all negation inwards to the propositions. It is assumed that the Boolean expression
* comprises only the operators !, & and |. Anything else is treated as a proposition.
* The passed in expression is modified, and the result is returned.
*/
private static Expression doConversionToPositiveNormalForm(Expression expr)
{
// Remove negation
if (Expression.isNot(expr)) {
Expression neg = ((ExpressionUnaryOp) expr).getOperand();
if (Expression.isNot(neg)) {
Expression a = ((ExpressionUnaryOp) neg).getOperand();
// !(!a) == a
return doConversionToPositiveNormalForm(a);
} else if (Expression.isOr(neg)) {
Expression a = ((ExpressionBinaryOp) neg).getOperand1();
Expression b = ((ExpressionBinaryOp) neg).getOperand2();
Expression aNeg = Expression.Not(a);
Expression bNeg = Expression.Not(b);
// !(a | b) == !a & !b
return doConversionToPositiveNormalForm(Expression.And(aNeg, bNeg));
} else if (Expression.isAnd(neg)) {
Expression a = ((ExpressionBinaryOp) neg).getOperand1();
Expression b = ((ExpressionBinaryOp) neg).getOperand2();
Expression aNeg = Expression.Not(a);
Expression bNeg = Expression.Not(b);
// !(a & b) == !a | !b
return doConversionToPositiveNormalForm(Expression.Or(aNeg, bNeg));
} else {
// Proposition (negated)
return expr;
}
}
// Preserve and
if (Expression.isAnd(expr)) {
Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1());
Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2());
return Expression.And(a, b);
}
// Preserve or
if (Expression.isOr(expr)) {
Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1());
Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2());
return Expression.Or(a, b);
}
// Proposition
return expr;
}
/**
* Convert an expression to disjunctive normal form (DNF).
* The passed in expression is modified, and the result is returned.
*/
public static Expression convertToDNF(Expression expr) throws PrismException
{
return convertDNFListsToExpression(doConversionToDNF(convertToPositiveNormalForm(expr)));
}
/**
* Convert an expression to disjunctive normal form (DNF).
* The passed in expression is modified, and the result is returned as a list of lists of Expression;
*/
public static List<List<Expression>> convertToDNFLists(Expression expr) throws PrismException
{
return doConversionToDNF(convertToPositiveNormalForm(expr));
}
private static List<List<Expression>> doConversionToDNF(Expression expr)
{
// And
if (Expression.isAnd(expr)) {
Expression a = ((ExpressionBinaryOp) expr).getOperand1();
Expression b = ((ExpressionBinaryOp) expr).getOperand2();
List<List<Expression>> aDnf = doConversionToDNF(a);
List<List<Expression>> bDnf = doConversionToDNF(b);
// a1|a2|... & b1|b2|... == a1&b1 | a1&b2 | ...
List<List<Expression>> dnf = new ArrayList<List<Expression>>();
for (List<Expression> ai : aDnf) {
for (List<Expression> bj : bDnf) {
List<Expression> aibj = new ArrayList<Expression>();
aibj.addAll(ai);
aibj.addAll(bj);
dnf.add(aibj);
}
}
return dnf;
}
// Or
if (Expression.isOr(expr)) {
Expression a = ((ExpressionBinaryOp) expr).getOperand1();
Expression b = ((ExpressionBinaryOp) expr).getOperand2();
List<List<Expression>> aDnf = doConversionToDNF(a);
List<List<Expression>> bDnf = doConversionToDNF(b);
// (a1|a2|...) | (b1|b2|...) == a1|a2|...|b1|b2|...
aDnf.addAll(bDnf);
return aDnf;
}
// Convert proposition to trivial DNF
List<List<Expression>> dnf = new ArrayList<List<Expression>>(1);
List<Expression> disjunct = new ArrayList<Expression>(1);
disjunct.add(expr);
dnf.add(disjunct);
return dnf;
}
/**
* Convert an expression to conjunctive normal form (CNF).
* The passed in expression is modified, and the result is returned.
*/
public static Expression convertToCNF(Expression expr) throws PrismException
{
return convertCNFListsToExpression(doConversionToCNF(convertToPositiveNormalForm(expr)));
}
/**
* Convert an expression to conjunctive normal form (CNF).
* The passed in expression is modified, and the result is returned as a list of lists of Expression;
*/
public static List<List<Expression>> convertToCNFLists(Expression expr) throws PrismException
{
return doConversionToCNF(convertToPositiveNormalForm(expr));
}
private static List<List<Expression>> doConversionToCNF(Expression expr)
{
// Remove parentheses
if (Expression.isParenth(expr)) {
return doConversionToCNF(((ExpressionUnaryOp) expr).getOperand());
}
// Or
if (Expression.isOr(expr)) {
Expression a = ((ExpressionBinaryOp) expr).getOperand1();
Expression b = ((ExpressionBinaryOp) expr).getOperand2();
List<List<Expression>> aCnf = doConversionToCNF(a);
List<List<Expression>> bCnf = doConversionToCNF(b);
// a1&a2&... | b1&b2&... == a1|b1 & a1|b2 & ...
List<List<Expression>> cnf = new ArrayList<List<Expression>>();
for (List<Expression> ai : aCnf) {
for (List<Expression> bj : bCnf) {
List<Expression> aibj = new ArrayList<Expression>();
aibj.addAll(ai);
aibj.addAll(bj);
cnf.add(aibj);
}
}
return cnf;
}
// Or
if (Expression.isOr(expr)) {
Expression a = ((ExpressionBinaryOp) expr).getOperand1();
Expression b = ((ExpressionBinaryOp) expr).getOperand2();
List<List<Expression>> aCnf = doConversionToCNF(a);
List<List<Expression>> bCnf = doConversionToCNF(b);
// (a1|a2|...) | (b1|b2|...) == a1|a2|...|b1|b2|...
aCnf.addAll(bCnf);
return aCnf;
}
// Convert proposition to trivial CNF
List<List<Expression>> cnf = new ArrayList<List<Expression>>(1);
List<Expression> conjunct = new ArrayList<Expression>(1);
conjunct.add(expr);
cnf.add(conjunct);
return cnf;
}
// Methods to convert And/Or classes to Expressions
public static Expression convertDNFListsToExpression(List<List<Expression>> dnf)
{
Expression ret = convertConjunctionListToExpression(dnf.get(0));
for (int i = 1; i < dnf.size(); i++) {
ret = Expression.Or(ret, convertConjunctionListToExpression(dnf.get(i)));
}
return ret;
}
public static Expression convertCNFListsToExpression(List<List<Expression>> cnf)
{
Expression ret = convertDisjunctionListToExpression(cnf.get(0));
for (int i = 1; i < cnf.size(); i++) {
ret = Expression.And(ret, convertDisjunctionListToExpression(cnf.get(i)));
}
return ret;
}
public static Expression convertDisjunctionListToExpression(List<Expression> disjunction)
{
Expression ret = disjunction.get(0);
for (int i = 1; i < disjunction.size(); i++) {
ret = Expression.Or(ret, disjunction.get(i));
}
return ret;
}
public static Expression convertConjunctionListToExpression(List<Expression> conjunction)
{
Expression ret = conjunction.get(0);
for (int i = 1; i < conjunction.size(); i++) {
ret = Expression.And(ret, conjunction.get(i));
}
return ret;
}
// Test code
public static void main(String args[])
{
PrismParser parser = new PrismParser();
String ss[] = new String[] { "a&!(b=>c)", "(a|b)&(c|d|e)" };
for (String s : ss) {
try {
Expression expr = parser.parseSingleExpression(new ByteArrayInputStream(s.getBytes()));
System.out.println(expr + " in CNF is " + convertToCNF(expr.deepCopy()));
System.out.println(expr + " in DNF is " + convertToDNF(expr.deepCopy()));
} catch (PrismException e) {
System.out.println("Error: " + e.getMessage());
}
}
}
}

27
prism/src/parser/ast/RelOp.java
View File

@ -5,6 +5,8 @@ import java.util.Iterator;
import java.util.Map;
import java.util.Map.Entry;
import prism.PrismLangException;
/**
* Class to represent a relational operator (or similar) found in a P/R/S operator.
*/
@ -100,6 +102,31 @@ public enum RelOp {
}
}
/**
* Returns the negated form of this operator.
*/
public RelOp negate() throws PrismLangException
{
switch (this) {
case GT:
return RelOp.LEQ;
case GEQ:
return RelOp.LT;
case MIN:
return RelOp.MAX;
case LT:
return RelOp.GEQ;
case LEQ:
return RelOp.GT;
case MAX:
return RelOp.MIN;
case EQ:
throw new PrismLangException("Cannot negate =");
default:
throw new PrismLangException("Cannot negate " + this);
}
}
/**
* Returns the RelOp object corresponding to a (string) symbol,
* e.g. parseSymbol("&lt;=") returns RelOp.LEQ. Returns null if invalid.

82
prism/src/prism/NondetModelChecker.java
View File

@ -43,6 +43,7 @@ import jdd.JDDNode;
import jdd.JDDVars;
import mtbdd.PrismMTBDD;
import odd.ODDUtils;
import parser.BooleanUtils;
import parser.ast.Coalition;
import parser.ast.Expression;
import parser.ast.ExpressionFunc;
@ -55,6 +56,7 @@ import parser.ast.ExpressionUnaryOp;
import parser.ast.PropertiesFile;
import parser.ast.RelOp;
import parser.type.TypeBool;
import parser.type.TypeDouble;
import parser.type.TypePathBool;
import parser.type.TypePathDouble;
import sparse.PrismSparse;
@ -199,22 +201,22 @@ public class NondetModelChecker extends NonProbModelChecker
coalition = null;
}
// Strip any parentheses (they might have been needlessly wrapped around a single P or R)
// Strip any parentheses
Expression exprSub = expr.getExpression();
while (Expression.isParenth(exprSub))
exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
// Pass onto relevant method:
// P operator
// Single P operator
if (exprSub instanceof ExpressionProb) {
return checkExpressionProb((ExpressionProb) exprSub, forAll);
}
// R operator
// Single R operator
else if (exprSub instanceof ExpressionReward) {
return checkExpressionReward((ExpressionReward) exprSub, forAll);
}
// Anything else is an error
// Anything else is treated as multi-objective
else {
throw new PrismException("Unexpected operators in " + expr.getOperatorString() + " operator");
return checkExpressionMultiObjective(expr, forAll);
}
}
@ -347,6 +349,76 @@ public class NondetModelChecker extends NonProbModelChecker
}
}
protected StateValues checkExpressionMultiObjective(ExpressionStrategy expr, boolean forAll) throws PrismException
{
// Copy expression because we will modify it
expr = (ExpressionStrategy) expr.deepCopy();
// Strip any outer parentheses in operand
Expression exprSub = expr.getExpression();
while (Expression.isParenth(exprSub)) {
exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
}
// Reduce to form that can be expressed as an old multi(...) function..
// Boolean
if (exprSub.getType() instanceof TypeBool) {
// We will solve an existential query, so negate if universal
if (forAll) {
exprSub = Expression.Not(exprSub);
}
// Convert to DNF
List<List<Expression>> dnf = BooleanUtils.convertToDNFLists(exprSub);
// Check all "propositions" of DNF are valid
for (List<Expression> conjunction : dnf) {
for (Expression prop : conjunction) {
if (Expression.isNot(prop)) {
prop = ((ExpressionUnaryOp) prop).getOperand();
}
if (!(prop instanceof ExpressionQuant)) {
throw new PrismException("Expression " + prop + " is not allowed in a multi-objective query");
}
}
}
// Push negation inside objectives
for (List<Expression> conjunction : dnf) {
for (int j = 0; j < conjunction.size(); j++) {
Expression prop = conjunction.get(j);
if (Expression.isNot(prop)) {
ExpressionQuant exprQuant = (ExpressionQuant) ((ExpressionUnaryOp) prop).getOperand();
exprQuant.setRelOp(exprQuant.getRelOp().negate());
conjunction.set(j, exprQuant);
}
}
}
// Print reduced query
mainLog.println("\nReducing multi-objective query to DNF: " + BooleanUtils.convertDNFListsToExpression(dnf));
// Only handle a single disjunct for now
if (dnf.size() > 1) {
throw new PrismException("Multi-objective model checking of multiople disjuncts not yet supported");
}
// Convert to multi(...)
ExpressionFunc exprMulti = new ExpressionFunc("multi");
for (Expression conjunct : dnf.get(0)) {
exprMulti.addOperand(conjunct);
}
// Handle negation
if (forAll) {
return checkExpression(Expression.Not(exprMulti));
} else {
return checkExpressionMultiObjective(exprMulti);
}
} else if (exprSub.getType() instanceof TypeDouble) {
ExpressionFunc exprMulti = new ExpressionFunc("multi");
exprMulti.addOperand(exprSub);
return checkExpressionMultiObjective(exprMulti);
} else {
throw new PrismException("Multi-objective model checking not supported for: " + exprSub);
}
}
/**
* Model check a multi-objective expression and return the result.
* For multi-objective queries, we only find the value for one state.

Write Preview
Loading…
Cancel
Save