diff --git a/prism/src/prism/ModelExpressionTransformation.java b/prism/src/prism/ModelExpressionTransformation.java new file mode 100644 index 00000000..bce63621 --- /dev/null +++ b/prism/src/prism/ModelExpressionTransformation.java @@ -0,0 +1,54 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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 prism; + +import parser.ast.Expression; + +/** + * Interface for a model and expression transformation.
+ * + * Implementing classes provide a combined model and expression transformation, allowing the calculation + * of a (potentially simpler) expression in the transformed model to calculate the result of the + * original expression in the original model.
+ * + * The general idea is the following sequence of calls:
+ * + * {@code ModelExpressionTransformation t = ...;}
+ * {@code StateValues resultTransformed = check t.getTransformedExpression() in t.getTransformedModel()}
+ * {@code StateValues result = t.projectToOriginalModel(resultTransformed);} + */ +public interface ModelExpressionTransformation + extends ModelTransformation { + + /** Get the transformed expression. */ + public Expression getTransformedExpression(); + + /** Get the original expression. */ + public Expression getOriginalExpression(); + +} diff --git a/prism/src/prism/ModelExpressionTransformationNested.java b/prism/src/prism/ModelExpressionTransformationNested.java new file mode 100644 index 00000000..6c60d842 --- /dev/null +++ b/prism/src/prism/ModelExpressionTransformationNested.java @@ -0,0 +1,108 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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 prism; + +import jdd.JDDNode; +import parser.ast.Expression; +import prism.PrismException; + +/** + * Nesting of two model/expression transformations. + *
+ * original -(innerTransformation)-> intermediate -(outerTransformation)-> transformed + */ + +public class ModelExpressionTransformationNested implements + ModelExpressionTransformation { + + /** The inner transformation */ + protected ModelExpressionTransformation innerTransformation; + /** The outer transformation */ + protected ModelExpressionTransformation outerTransformation; + + /** + * Constructor, chain the two transformations. + *
+ * The transformations will be cleared on a call to {@code clear()}. + *
+ * [STORE: innerTransformation, outerTransformation ] + */ + public ModelExpressionTransformationNested(ModelExpressionTransformation innerTransformation, + ModelExpressionTransformation outerTransformation) + { + this.innerTransformation = innerTransformation; + this.outerTransformation = outerTransformation; + + if (innerTransformation.getTransformedModel() != outerTransformation.getOriginalModel()) { + throw new IllegalArgumentException("Trying to nest unrelated ModelExpressionTransformations."); + } + } + + @Override + public TransformedModel getTransformedModel() + { + return outerTransformation.getTransformedModel(); + } + + @Override + public StateValues projectToOriginalModel(StateValues svTransformedModel) throws PrismException + { + StateValues svIntermediate = outerTransformation.projectToOriginalModel(svTransformedModel); + StateValues svOriginal = innerTransformation.projectToOriginalModel(svIntermediate); + return svOriginal; + } + + @Override + public Expression getTransformedExpression() + { + return outerTransformation.getTransformedExpression(); + } + + @Override + public OriginalModel getOriginalModel() { + return innerTransformation.getOriginalModel(); + } + + @Override + public Expression getOriginalExpression() + { + return innerTransformation.getOriginalExpression(); + } + + @Override + public JDDNode getTransformedStatesOfInterest() + { + return outerTransformation.getTransformedStatesOfInterest(); + } + + @Override + public void clear() + { + outerTransformation.clear(); + innerTransformation.clear(); + } +} \ No newline at end of file diff --git a/prism/src/prism/ModelTransformation.java b/prism/src/prism/ModelTransformation.java new file mode 100644 index 00000000..25d36d36 --- /dev/null +++ b/prism/src/prism/ModelTransformation.java @@ -0,0 +1,68 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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 prism; + +import jdd.JDDNode; +import prism.PrismException; + +/** + * Interface for a model transformation. + */ +public interface ModelTransformation { + + /** Get the original model. */ + public OriginalModel getOriginalModel(); + + /** Get the transformed model. */ + public TransformedModel getTransformedModel(); + + /** Clear the transformed model and all other intermediate BDD information. + * Should be called when the transformation is not needed anymore. Does not clear the + * original model. + */ + public void clear(); + + /** + * Take a {@code StateValues} object for the transformed model and + * project the values to the original model. + *
+ * The {@code svTransformedModel} argument is consumed/cleared and should not be + * used afterwards. + * @param svTransformedModel a {@code StateValues} object for the transformed model + * @return a corresponding {@code StateValues} object for the original model. + */ + public StateValues projectToOriginalModel(StateValues svTransformedModel) throws PrismException; + + /** + * Get the transformed state set of the states of interest, + * i.e., the set of states that should be calculated to allow a successful + * application of the projectToOriginalModel method. + * + *
[REF: result] + */ + public JDDNode getTransformedStatesOfInterest(); +} diff --git a/prism/src/prism/ModelTransformationNested.java b/prism/src/prism/ModelTransformationNested.java new file mode 100644 index 00000000..6eb44b84 --- /dev/null +++ b/prism/src/prism/ModelTransformationNested.java @@ -0,0 +1,95 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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 prism; + +import jdd.JDDNode; +import prism.PrismException; + +/** + * Nesting of two model transformations. + *
+ * originalModel -(innerTransformation)-> intermediateModel -(outerTransformation)-> transformedModel + */ +public class ModelTransformationNested implements + ModelTransformation { + + /** The inner transformation */ + protected ModelTransformation innerTransformation; + /** The outer transformation */ + protected ModelTransformation outerTransformation; + + /** + * Constructor, chain the two transformations. + *
+ * The transformations will be cleared on a call to {@code clear()}. + *
+ * [STORE: innerTransformation, outerTransformation ] + */ + public ModelTransformationNested(ModelTransformation innerTransformation, + ModelTransformation outerTransformation) throws PrismException + { + this.innerTransformation = innerTransformation; + this.outerTransformation = outerTransformation; + + if (innerTransformation.getTransformedModel() != outerTransformation.getOriginalModel()) { + throw new PrismException("Trying to nest unrelated ModelExpressionTransformations."); + } + } + + @Override + public TransformedModel getTransformedModel() + { + return outerTransformation.getTransformedModel(); + } + + @Override + public StateValues projectToOriginalModel(StateValues svTransformedModel) throws PrismException + { + StateValues svIntermediate = outerTransformation.projectToOriginalModel(svTransformedModel); + StateValues svOriginal = innerTransformation.projectToOriginalModel(svIntermediate); + return svOriginal; + } + + @Override + public OriginalModel getOriginalModel() + { + return innerTransformation.getOriginalModel(); + } + + @Override + public void clear() + { + outerTransformation.clear(); + innerTransformation.clear(); + } + + @Override + public JDDNode getTransformedStatesOfInterest() + { + return outerTransformation.getTransformedStatesOfInterest(); + } +}