Commit 0053835e authored by Benoit Barbot's avatar Benoit Barbot
Browse files

Merge change for Qest 2016 computing splitPTA from forward reachability graph

parent 8394df8e
Pipeline #1257 failed with stages
in 17 seconds
......@@ -37,11 +37,7 @@ import java.util.List;
import common.StackTraceHelper;
import parser.Values;
import parser.ast.Expression;
import parser.ast.ExpressionReward;
import parser.ast.ModulesFile;
import parser.ast.PropertiesFile;
import parser.ast.Property;
import parser.ast.*;
import prism.Prism.StrategyExportType;
import simulator.GenerateSimulationPath;
import simulator.method.ACIconfidence;
......@@ -468,6 +464,22 @@ public class PrismCL implements PrismModelListener
}
}
//Build dummy expression to force the computation reachability region graph in order to export it.
if(prism.settings.getString(PrismSettings.PRISM_PTA_MAXENTROPY_PATH) != ""){
try {
ExpressionTemporal dummi = new ExpressionTemporal(ExpressionTemporal.P_F, Expression.True(),
Expression.True());
dummi.convertToUntilForm();
prism.modelCheckPTA(propertiesFile, new ExpressionProb( dummi, "max=", null) , null );
} catch (PrismException e) {
// in case of (overall) error, report it, store as result for property, and proceed
error(e.getMessage());
results[j].setMultipleErrors(definedMFConstants, null, e);
continue;
}
}
// Explicitly request a build if necessary
if (propertiesToCheck.size() == 0 && !steadystate && !dotransient && !simpath && !nobuild && prism.modelCanBeBuilt() && !prism.modelIsBuilt()) {
try {
......
......@@ -110,6 +110,7 @@ public class PrismSettings implements Observer
public static final String PRISM_SYMM_RED_PARAMS = "prism.symmRedParams";
public static final String PRISM_EXACT_ENABLED = "prism.exact.enabled";
public static final String PRISM_PTA_METHOD = "prism.ptaMethod";
public static final String PRISM_PTA_MAXENTROPY_PATH = "prism.ptaMaxEntropyPath";
public static final String PRISM_TRANSIENT_METHOD = "prism.transientMethod";
public static final String PRISM_AR_OPTIONS = "prism.arOptions";
public static final String PRISM_PATH_VIA_AUTOMATA = "prism.pathViaAutomata";
......@@ -324,6 +325,8 @@ public class PrismSettings implements Observer
"Maximum memory available to CUDD (underlying BDD/MTBDD library), e.g. 125k, 50m, 4g. Note: Restart PRISM after changing this." },
{ DOUBLE_TYPE, PRISM_CUDD_EPSILON, "CUDD epsilon", "2.1", new Double(1.0E-15), "0.0,",
"Epsilon value used by CUDD (underlying BDD/MTBDD library) for terminal cache comparisons." },
{ STRING_TYPE, PRISM_PTA_MAXENTROPY_PATH, "Path for the output of PTA rechability graph", "4.5", "", "Digital clocks,Stochastic games",
"Use for max entropy distribution computation." },
{ INTEGER_TYPE, PRISM_DD_EXTRA_STATE_VARS, "Extra DD state var allocation", "4.3.1", new Integer(20), "",
"Number of extra DD state variables preallocated for use in model transformation." },
{ INTEGER_TYPE, PRISM_DD_EXTRA_ACTION_VARS, "Extra DD action var allocation", "4.3.1", new Integer(20), "",
......@@ -1001,6 +1004,17 @@ public class PrismSettings implements Observer
else if (sw.equals("exact")) {
set(PRISM_EXACT_ENABLED, true);
}
// PTA splitted rechability graph export
else if (sw.equals("exportsplitreach")) {
if (i < args.length - 1) {
set(PRISM_PTA_MAXENTROPY_PATH,args[++i]);
} else {
throw new PrismException("No parameter specified for -" + sw + " switch");
}
}
// PTA model checking methods
else if (sw.equals("ptamethod")) {
if (i < args.length - 1) {
......
......@@ -41,7 +41,7 @@ public class Constraint
* @param y Right clock
* @param db Difference bound encoded as an integer
*/
private Constraint(int x, int y, int db)
public Constraint(int x, int y, int db)
{
this.x = x;
this.y = y;
......@@ -201,4 +201,9 @@ public class Constraint
{
return new Constraint(y, x, DB.createLt(-v));
}
public Constraint openIt()
{
return new Constraint(x,y,DB.openIt(db));
}
}
......@@ -60,6 +60,17 @@ public class DB
return (DIFF_MASK & d) >> 1;
}
// Get absolute difference part of bound
protected static int getAbsoluteDiff(int d)
{int res= getSignedDiff(d);
if (res<0){return -res;}
return res;
}
// return true if the absolute bounds are the same whatever independently of <, \leq.
protected static boolean compareBounds(int d_1, int d_2)
{ return(getAbsoluteDiff(d_1)==getAbsoluteDiff(d_2));
}
// Is bound strict?
protected static boolean isStrict(int d)
{
......@@ -91,6 +102,22 @@ public class DB
return isStrict(d) ? createLeq(-getSignedDiff(d)) : createLt(-getSignedDiff(d));
}
protected static int opposite(int d)
{
if (d == INFTY)
return d;
// TODO: probably a more efficient way to do this
return !isStrict(d) ? createLeq(-getSignedDiff(d)) : createLt(-getSignedDiff(d));
}
protected static int openIt(int d)
{
if (d == INFTY)
return d;
// TODO: probably a more efficient way to do this
return createLt(getSignedDiff(d));
}
// Get bound as a string
protected static String toString(int d)
{
......@@ -177,4 +204,11 @@ public class DB
}
return s;
}
public static int closeIt(int i)
{
if (i == INFTY)
return i;
return createLeq(getSignedDiff(i));
}
}
......@@ -26,6 +26,10 @@
package pta;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;
/**
* Implementation of the difference-bound matrix (DBM) data structure.
*
......@@ -66,6 +70,12 @@ public class DBM extends Zone
// Zone operations (modify the zone)
public DBM(PTA pta, int d[][])
{
this.pta = pta;
this.d = d;
}
/**
* Conjunction: add constraint x-y db
*/
......@@ -477,7 +487,7 @@ public class DBM extends Zone
/**
* Canonicalise, by applying Floyd-Warshall SPP algorithm
*/
private void canonicalise()
protected void canonicalise()
{
int k, i, j, db, n;
n = pta.numClocks;
......@@ -542,4 +552,167 @@ public class DBM extends Zone
}
return dbm;
}
/**
* Zone defined by set of constraints
*/
public static DBM createFromTransition(Transition tr)
{
DBM dbm = createTrue(tr.getParent());
for (Constraint c : tr.guard) {
dbm.addConstraint(c);
}
return dbm;
}
public Set<Constraint> toConstraint(){
int n = pta.numClocks;
Set<Constraint> res = new HashSet<Constraint>();
for (int i = 0; i < n + 1; i++) {
for (int j = 0; j < n + 1; j++) {
//Constraint res_aux = new Constraint(i, j, d[i][j]);
res.add(new Constraint(i, j, d[i][j]));
}
}
return res;
}
//returns wether the (upper if b, lower if not b) bound on x_i is useless
public boolean isUseless(int i, boolean b){
PTA pta = this.getPTA();
int n = pta.numClocks + 1;
boolean acc = false;
if (b){
for (int j = 1; j < n & !acc; j++){
if (j != i) {acc = (acc || (this.d[i][0] >= DB.add(this.d[i][j], this.d[j][0])));}
}
}
else{
for (int j = 1; j < n & !acc; j++){
if (j != i) {acc = (acc || (this.d[0][i] >= DB.add(this.d[0][j] ,this.d[j][i])));}
}
}
return acc;
}
//remove useless constant constraints
public void reduce(){
this.canonicalise();
PTA pta = this.getPTA();
int n = pta.numClocks + 1;
for(int i = 0; i < n; i++){
if (this.isUseless(i,true)){
this.d[i][0] = DB.INFTY;
//System.out.printf("\n est inutile : x_%d, upper",i);
}
if (this.isUseless(i,false)){
//System.out.printf("\n est inutile : x_%d, lower",i);
this.d[0][i] = DB.INFTY;
}
}
}
public void PunctualtoEmpty(){}
//return upper and lower bound to string; assuming there is no more corner
public String PrintLowerandUpper(){
String s="";
this.reduce();
PTA pta = this.getPTA();
int n = pta.numClocks + 1;
for(int i = 1; i < n; i++){
if (this.d[0][i] != DB.INFTY){
int val= DB.getAbsoluteDiff(this.d[0][i]);
if (val == 0){
s+=0+" , "+0;break;
}
else{
s+=val+" , "+i;break;
}
}
}
for(int i = 1; i < n; i++){
if (this.d[i][0] != DB.INFTY){
s+= " , " + DB.getAbsoluteDiff(this.d[i][0])+" , "+i;break;
}
}
return s;
}
public boolean openIt(Zone z){
DBM m= (DBM) z;
m.canonicalise();//TODO remove this if already canonical
int i, j, n;
n = pta.numClocks;
for (i = 0; i < n + 1; i++) {
for (j = i+1; j < n + 1; j++) {
if (!DB.compareBounds(m.d[i][j], m.d[j][i]))//We keep equality, and open non punctual intervals.
{d[i][j]=DB.openIt(d[i][j]);
d[j][i]=DB.openIt(d[j][i]);
}
}
this.canonicalise();//to see whether the zone is empty or not.
}
return(this.isEmpty());
}
//The following is to be used for guard only.
public boolean isPunctual(){
this.canonicalise();
int n = pta.numClocks + 1;
for(int i = 1; i < n; i++){
if(d[i][0]<=1 | DB.compareBounds(d[i][0],d[0][i])){
return true;}
for(int j =i+1 ; j < n; j++){
if(!DB.isInfty(d[i][j]) & DB.compareBounds(d[i][j],d[j][i])& (DB.getSignedDiff(d[i][j])!=0)){
return true;}
}
}
return false;
}
/***
*
* @return a list of list of index of clocks which are pairwise equals (the fist list is the clocks equals to 0) and the first element of each list is the smallest index.
*/
public ArrayList<ArrayList<Integer>> reducedCoordinate(){
ArrayList<ArrayList<Integer>> res= new ArrayList<ArrayList<Integer>>();
//System.out.printf("%s",res.toString());
int i, j, n;
n = pta.numClocks;
int[] rC =new int [n+1];
ArrayList<Integer> zeroList=new ArrayList<Integer>();
//System.out.printf("%s",zeroList.toString());
zeroList.add(0);
//System.out.printf("%s",zeroList.toString());
for (i = 1; i < n + 1; i++) {
if (d[i][0]<2)
{rC[i]=0;zeroList.add(i);}
else
{rC[i]=i;}
}
//System.out.printf("%s",zeroList.toString());
int numParts=0;//the number of parts
res.add(zeroList);
//System.out.printf("%s",res.toString());
for (i = 1; i < n + 1; i++) {
if (rC[i]!=i) {continue;}//This clocks is already equals to another, continue!
numParts++;
rC[i]=numParts;
ArrayList<Integer> newList=new ArrayList<Integer>();
newList.add(i);
res.add(newList);
for (j = i+1; j < n + 1; j++) {
if (DB.compareBounds(d[i][j], d[j][i]))
{rC[j]=rC[i];res.get(numParts).add(j);}
}
}
//System.out.printf("\n%s %s \n",this.toString(),res.toString());
return(res);
}
}
......@@ -53,6 +53,18 @@ public class DBMList extends NCZone
list = new ArrayList<DBM>();
}
public Set<Constraint> toConstraint()
{
Set<Constraint> res = new HashSet();
for(DBM dbm : list){
Set<Constraint> res_aux = dbm.toConstraint();
for(Constraint res_aux_aux : res_aux){
res.add(res_aux_aux);
}
}
return res;
}
/**
* Copy constructor: create single list from existing DBM(List)
*/
......@@ -129,6 +141,12 @@ public class DBMList extends NCZone
return list.get(i);
}
public ArrayList<DBM> getList()
{
return list;
}
// Methods required for Zone interface
/**
......@@ -283,6 +301,17 @@ public class DBMList extends NCZone
return dbml;
}
/**
* Complement as above without punctual guard
*/
public DBMList createComplementnonPunctual()
{
DBMList dbml = deepCopy();
dbml.complementwithoutPunctuality();
return dbml;
}
// Zone queries (do not modify the zone)
/**
......@@ -418,6 +447,35 @@ public class DBMList extends NCZone
list = res.list;
}
/**
* Complement
*/
public void complementwithoutPunctuality()
{
DBMList listNew, res;
res = null;
// Special case: complement of empty DBM list is True
if (list.size() == 0)
addDBM(DBM.createTrue(pta));
// The complement of a list of DBMs is the intersection
// of the complement of each DBM (and the complement of
// of a DBM is a DBM list).
for (DBM dbm : list) {
listNew = dbm.createComplement();
if (res == null)
res = listNew;
else {
res.intersect(listNew);
}
// Stop early if res already empty
if (res.list.size() == 0)
break;
}
list = res.list;
removeInclusionsandPunctuality();
}
/**
* Disjunction: with another zone
*/
......@@ -551,7 +609,41 @@ public class DBMList extends NCZone
list.remove(i);
}
}
/***Not implemented
*
*/
public ArrayList<ArrayList<Integer>> reducedCoordinate(){return new ArrayList<ArrayList<Integer>>();};
private void removeInclusionsandPunctuality()
{
int i, j, n;
DBM dbm1, dbm2;
BitSet toRemove;
n = list.size();
toRemove = new BitSet(n);
for (i = 0; i < n; i++) {
if (toRemove.get(i))
continue;
dbm1 = list.get(i);
dbm1.PunctualtoEmpty();
if (dbm1.isEmpty()){toRemove.set(i); continue;}
for (j = i + 1; j < n; j++) {
if (toRemove.get(i) || toRemove.get(j))
continue;
dbm2 = list.get(j);
if (dbm2.includes(dbm1))
toRemove.set(i);
else if (dbm1.includes(dbm2))
toRemove.set(j);
}
}
for (i = n - 1; i >= 0; i--) {
if (toRemove.get(i))
list.remove(i);
}
}
// Test program for complementing big DBM lists
public static void main(String args[])
......
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of 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 pta;
import java.util.*;
public class DBMandBound extends DBM
{
public LinkedList<Integer> lowerbounds;
public LinkedList<Integer> upperbounds;
/**
* Construct an empty DBMandBound
*/
public DBMandBound(PTA pta)
{
super(pta);
this.lowerbounds= new LinkedList<Integer>();
this.upperbounds= new LinkedList<Integer>();
}
public DBMandBound (DBM M){
super(M.pta);
LinkedList<Integer> upperbounds = new LinkedList<Integer>();
LinkedList<Integer> lowerbounds = new LinkedList<Integer>();
M.reduce();
PTA pta = M.getPTA();
int n = pta.numClocks + 1;
//lower bounds
for(int i = 1; i < n; i++){
if (M.d[0][i] != DB.INFTY){
lowerbounds.add(i);
}
}
//upper bounds
for(int i = 1; i < n; i++){
if (M.d[i][0] != DB.INFTY){
upperbounds.add(i);
}
}
this.pta =M.pta;
this.d =M.d;
this.upperbounds=upperbounds;
this.lowerbounds=lowerbounds;
}
//Basic test not used
// public boolean isUpperSplitted(){
// return (upperbounds.size()==1);
// }
//
// public boolean isLowerSplitted(){
// return (lowerbounds.size()==1);
// }
// public boolean isSplitted(){
// return (this.isUpperSplitted()&this.isLowerSplitted());
// }
//assuming that there is only one lower bound return it
// public int getLB() {
// return DB.getAbsoluteDiff(d[0][lowerbounds.get(0)]);
// }
//assuming that there is only one upper bound return it
// public int getUB() {
// return DB.getAbsoluteDiff(d[upperbounds.get(0)][0]);
// }
// public boolean isPunctual()
// {
// }
public DBMandBound CopyWithoutUB()
{
int i, j, n;
DBMandBound copy = new DBMandBound(pta);
n = this.pta.numClocks;
copy.d = new int[n + 1][n + 1];
for (i = 0; i < n + 1; i++) {
for (j = 0; j < n + 1; j++) {
copy.d[i][j] = d[i][j];
}
}
copy.lowerbounds=this.lowerbounds;
return copy;
}
public DBMandBound CopyWithoutLB()
{
int i, j, n;
DBMandBound copy = new DBMandBound(pta);
n = this.pta.numClocks;
copy.d = new int[n + 1][n + 1];
for (i = 0; i < n + 1; i++) {
for (j = 0; j < n + 1; j++) {
copy.d[i][j] = d[i][j];
}
}
copy.upperbounds=this.upperbounds;
return copy;
}
public LinkedList<DBMandBound> lowerSplit(){
LinkedList<DBMandBound> res = new LinkedList<DBMandBound>();
int k = lowerbounds.size();
for (int i = 0; i < k; i++){
int g = lowerbounds.get(i);
DBMandBound res_aux;
res_aux=this.CopyWithoutLB();
res_aux.lowerbounds.add(g);
for(int j = 0; j < k; j++ ){
if (j != i){
//res_aux.setConstraint(0, lowerbounds.get(j), 0);//useful?
res_aux.addConstraint(g,lowerbounds.get(j), DB.add(this.d[0][lowerbounds.get(j)], DB.opposite((this.d[0][g]))));
}