Updated Conversion
This commit is contained in:
LukasBuecherl
parent
75911f5931
commit
5453e5031d
1 changed files with 80 additions and 230 deletions
|
|
@ -21,6 +21,7 @@ import java.io.FilenameFilter;
|
|||
import java.io.IOException;
|
||||
import java.net.URI;
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.HashSet;
|
||||
import java.util.LinkedList;
|
||||
import java.util.List;
|
||||
|
|
@ -76,47 +77,23 @@ import edu.utah.ece.async.ibiosim.dataModels.util.GlobalConstants;
|
|||
*/
|
||||
public class SBML2PRISM {
|
||||
|
||||
|
||||
public static void GoodJob() //throws XMLStreamException, IOException, BioSimException
|
||||
{
|
||||
System.err.println("Good Job!");
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
* Convert SBML to Prism
|
||||
* Input: SBMLDocument, File
|
||||
* Output: void
|
||||
*
|
||||
* Function takes in a SBML document and writes the prism conversion of the file in the same directory. The function also translates the constraint into
|
||||
* a properties file that is written in the same directory in a separate file. The original filename is used for the prism and property file. The SBMML
|
||||
* file ends in .xml, the prism file in .sm, and the properties file in .props.
|
||||
*
|
||||
* To run the converter use the following command:
|
||||
* java -jar conversion/target/iBioSim-conversion-3.1.0-SNAPSHOT-jar-with-dependencies.jar -l PRISM YOURSBMLFILE.xml
|
||||
*/
|
||||
public static void convertSBML2PRISM(SBMLDocument sbmlDoc, String filename) throws IOException
|
||||
{
|
||||
Model model = sbmlDoc.getModel();
|
||||
File file = new File(filename.replace(".xml", ".sm"));
|
||||
|
||||
/*
|
||||
System.err.println("Species: ");
|
||||
for (int i = 0; i < model.getSpeciesCount(); i++)
|
||||
{
|
||||
Species species = model.getSpecies(i);
|
||||
System.err.println(species);
|
||||
}
|
||||
|
||||
System.err.println("Reactions: ");
|
||||
for (int i = 0; i < model.getReactionCount(); i++)
|
||||
{
|
||||
Reaction reaction = model.getReaction(i);
|
||||
System.err.println(reaction);
|
||||
|
||||
}
|
||||
|
||||
for (int i = 0; i < model.getConstraintCount(); i++)
|
||||
{
|
||||
System.err.println(SBMLutilities.convertMath2PrismProperty(model.getConstraint(i).getMath()));
|
||||
}
|
||||
|
||||
for (int i = 0; i < model.getParameterCount(); i++)
|
||||
{
|
||||
Parameter parameter = model.getParameter(i);
|
||||
System.err.println(parameter);
|
||||
}
|
||||
|
||||
*/
|
||||
|
||||
// Opening and writing preamble to the file
|
||||
FileWriter out = new FileWriter(file);
|
||||
out.write("// File generated by SBML-to-PRISM converter\n");
|
||||
|
|
@ -136,7 +113,7 @@ public class SBML2PRISM {
|
|||
for (int i = 0; i < model.getCompartmentCount(); i++)
|
||||
{
|
||||
Compartment compartment = model.getCompartment(i);
|
||||
out.write("const double " + compartment.getId() + " = " + compartment.getSize() + ";\n");
|
||||
out.write("const double " + checkReservedKeywordPrism(compartment.getId()) + " = " + compartment.getSize() + ";\n");
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -149,7 +126,7 @@ public class SBML2PRISM {
|
|||
for (int i = 0; i < model.getParameterCount(); i++)
|
||||
{
|
||||
Parameter parameter = model.getParameter(i);
|
||||
out.write("const double "+ parameter.getId() + " = " + parameter.getValue() +"; // " + parameter.getName() + "\n"); // if not null name
|
||||
out.write("const double "+ checkReservedKeywordPrism(parameter.getId()) + " = " + parameter.getValue() +"; // " + parameter.getName() + "\n"); // if not null name
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -159,12 +136,12 @@ public class SBML2PRISM {
|
|||
for (int i = 0; i < model.getSpeciesCount(); i++)
|
||||
{
|
||||
Species species = model.getSpecies(i);
|
||||
out.write("// Species " + species.getId() + "\n");
|
||||
out.write("// const int " + species.getId() + "_MAX = MAX_AMOUNT;\n");
|
||||
out.write("module "+ species.getId() + "\n");
|
||||
out.write("// Species " + checkReservedKeywordPrism(species.getId()) + "\n");
|
||||
out.write("// const int " + checkReservedKeywordPrism(species.getId()) + "_MAX = MAX_AMOUNT;\n");
|
||||
out.write("module "+ checkReservedKeywordPrism(species.getId()) + "\n");
|
||||
out.write("\n");
|
||||
out.write(" // "+ species.getId() +" : " + "[0.." + species.getId() + "_MAX] init "+ species.getInitialAmount() + ";\n");
|
||||
out.write(" "+ species.getId() + " : " + "int init " + species.getInitialAmount() + ";\n");
|
||||
out.write(" // "+ checkReservedKeywordPrism(species.getId()) +" : " + "[0.." + checkReservedKeywordPrism(species.getId()) + "_MAX] init "+ (int) species.getInitialAmount() + ";\n");
|
||||
out.write(" "+ checkReservedKeywordPrism(species.getId()) + " : " + "int init " + (int) (species.getInitialAmount()) + ";\n");
|
||||
out.write("\n");
|
||||
|
||||
for (int j = 0; j < model.getReactionCount(); j++)
|
||||
|
|
@ -176,12 +153,12 @@ public class SBML2PRISM {
|
|||
|
||||
if(reactant != null)
|
||||
{
|
||||
out.write(" // " + reaction.getId() + "\n");
|
||||
out.write(" [" + reaction.getId() + "] " + species.getId() + " > " + (reactant.getStoichiometry() - 1) + " -> (" + species.getId() + "\'=" + species.getId() + "-" + reactant.getStoichiometry() + ");\n");
|
||||
out.write(" // " + checkReservedKeywordPrism(reaction.getId()) + "\n");
|
||||
out.write(" [" + checkReservedKeywordPrism(reaction.getId()) + "] " + checkReservedKeywordPrism(species.getId()) + " > " + (int) (reactant.getStoichiometry() - 1) + " -> (" + checkReservedKeywordPrism(species.getId()) + "\'=" + checkReservedKeywordPrism(species.getId()) + "-" + (int) reactant.getStoichiometry() + ");\n");
|
||||
} else if (product != null)
|
||||
{
|
||||
out.write(" // " + reaction.getId() + "\n");
|
||||
out.write(" [" + reaction.getId() + "] " + species.getId() + " >= " + "0 -> (" + species.getId() + "\'=" + species.getId() + "+" + product.getStoichiometry() + ");\n");
|
||||
out.write(" // " + checkReservedKeywordPrism(reaction.getId()) + "\n");
|
||||
out.write(" [" + checkReservedKeywordPrism(reaction.getId()) + "] " + checkReservedKeywordPrism(species.getId()) + " >= " + "0 -> (" + checkReservedKeywordPrism(species.getId()) + "\'=" + checkReservedKeywordPrism(species.getId()) + "+" + (int) product.getStoichiometry() + ");\n");
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -192,7 +169,7 @@ public class SBML2PRISM {
|
|||
|
||||
}
|
||||
|
||||
// math
|
||||
// Identify reaction rates
|
||||
|
||||
out.write("// Reaction rates\n");
|
||||
out.write("module reaction_rates\n");
|
||||
|
|
@ -201,14 +178,14 @@ public class SBML2PRISM {
|
|||
for (int i = 0; i < model.getReactionCount(); i++)
|
||||
{
|
||||
Reaction reaction = model.getReaction(i);
|
||||
out.write(" // " + reaction.getId() + ": -> ");
|
||||
out.write(" // " + checkReservedKeywordPrism(reaction.getId()) + ": -> ");
|
||||
for(int j = 0; j < reaction.getProductCount(); j++)
|
||||
{
|
||||
out.write(reaction.getProduct(j).getSpecies() + " ");
|
||||
out.write(checkReservedKeywordPrism(reaction.getProduct(j).getSpecies()) + " ");
|
||||
}
|
||||
out.write("\n");
|
||||
|
||||
out.write(" [" + reaction.getId() + "] " + SBMLutilities.convertMath2PrismProperty(reaction.getKineticLaw().getMath()) + " > 0 -> " + "(" + SBMLutilities.convertMath2PrismProperty(reaction.getKineticLaw().getMath()) + ") : true;\n");
|
||||
out.write(" [" + checkReservedKeywordPrism(reaction.getId()) + "] " + checkReserveKeywordMath(SBMLutilities.convertMath2PrismProperty(reaction.getKineticLaw().getMath()), model) + " > 0 -> " + "(" + checkReserveKeywordMath(SBMLutilities.convertMath2PrismProperty(reaction.getKineticLaw().getMath()), model) + ") : true;\n");
|
||||
out.write("\n");
|
||||
|
||||
}
|
||||
|
|
@ -219,13 +196,13 @@ public class SBML2PRISM {
|
|||
out.write("\n");
|
||||
|
||||
|
||||
// Identify model species
|
||||
// Identify rewards
|
||||
for (int i = 0; i < model.getSpeciesCount(); i++)
|
||||
{
|
||||
Species species = model.getSpecies(i);
|
||||
|
||||
out.write("// Reward " + (i+1) + ": " + species.getId() + "\n");
|
||||
out.write("rewards " + "\"" + species.getId() + "\" true : " + species.getId() + "; endrewards\n");
|
||||
out.write("// Reward " + (i+1) + ": " + checkReservedKeywordPrism(species.getId()) + "\n");
|
||||
out.write("rewards " + "\"" + checkReservedKeywordPrism(species.getId()) + "\" true : " + checkReservedKeywordPrism(species.getId()) + "; endrewards\n");
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -242,198 +219,71 @@ public class SBML2PRISM {
|
|||
|
||||
for (int i = 0; i < model.getConstraintCount(); i++)
|
||||
{
|
||||
property_out.write(SBMLutilities.convertMath2PrismProperty(model.getConstraint(i).getMath()));
|
||||
System.err.println(checkReserveKeywordMath(SBMLutilities.convertMath2PrismProperty(model.getConstraint(i).getMath()), model));
|
||||
property_out.write(checkReserveKeywordMath(SBMLutilities.convertMath2PrismProperty(model.getConstraint(i).getMath()), model));
|
||||
}
|
||||
|
||||
property_out.close();
|
||||
|
||||
/*if (s.isConstant()) {
|
||||
// write const
|
||||
} else {
|
||||
// write modules
|
||||
}
|
||||
*/
|
||||
}
|
||||
|
||||
|
||||
|
||||
private static String checkReservedKeywordPrism(String speciesname)
|
||||
{
|
||||
|
||||
List<String> keywords = Arrays.asList("A", "bool", "clock", "const", "ctmc", "C", "double", "dtmc", "E", "endinit", "endinvariant", "endmodule",
|
||||
"endobservables", "endrewards", "endsystem", "false", "formula", "filter", "func", "F", "global", "G", "init", "invariant", "I", "int", "label",
|
||||
"max", "mdp", "min", "module", "X", "nondeterministic", "observable", "observables", "of", "Pmax", "Pmin", "P", "pomdp", "popta", "probabilistic",
|
||||
"prob", "pta", "rate", "rewards", "Rmax", "Rmin", "R", "S", "stochastic", "system", "true", "U", "W");
|
||||
|
||||
if (keywords.contains(speciesname))
|
||||
{
|
||||
return "_" + speciesname;
|
||||
}else {
|
||||
return speciesname;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
private static String checkReserveKeywordMath(String math, Model model) {
|
||||
|
||||
|
||||
|
||||
private int executePrism(String filename) throws IOException, InterruptedException, XMLStreamException, BioSimException {
|
||||
int exitValue = 255;
|
||||
String prop = null;
|
||||
String directory = properties.getDirectory() + File.separator;
|
||||
String out = properties.getModelFile().replace(".xml", "").replaceAll(".lpn", "").replaceAll(".sbml", "");
|
||||
LPN lhpnFile = null;
|
||||
// String root = properties.getRoot();
|
||||
|
||||
|
||||
new File(filename.replace(".gcm", "").replace(".sbml", "").replace(".xml", "") + ".lpn").delete();
|
||||
ArrayList<String> specs = new ArrayList<>();
|
||||
ArrayList<Object[]> conLevel = new ArrayList<>();
|
||||
retrieveSpeciesAndConLevels(specs, conLevel);
|
||||
BioModel bioModel = BioModel.createBioModel(properties.getDirectory(), this);
|
||||
bioModel.load(filename);
|
||||
if (bioModel.flattenModel(true) != null) {
|
||||
if (properties.getVerificationProperties().getLpnProperty() != null && !properties.getVerificationProperties().getLpnProperty().equals("")) {
|
||||
prop = properties.getVerificationProperties().getLpnProperty();
|
||||
} else {
|
||||
prop = properties.getVerificationProperties().getConstraintProperty();
|
||||
}
|
||||
MutableString mutProp = new MutableString(prop);
|
||||
lhpnFile = LPN.convertToLHPN(specs, conLevel, mutProp, bioModel);
|
||||
prop = mutProp.getString();
|
||||
if (lhpnFile == null) {
|
||||
new File(properties.getDirectory() + File.separator + "running").delete();
|
||||
return 0;
|
||||
}
|
||||
message.setLog("Saving SBML file as PRISM file:\n" + filename.replace(".xml", ".prism"));
|
||||
this.notifyObservers(message);
|
||||
message.setLog("Saving PRISM Property file:\n" + filename.replace(".xml", ".pctl"));
|
||||
this.notifyObservers(message);
|
||||
// TODO: LUKAS
|
||||
// bioModel.convertSBML2PRISM(logFile, filename);
|
||||
LPN.convertLPN2PRISM(logFile, lhpnFile, filename.replace(".xml", ".prism"), bioModel.getSBMLDocument());
|
||||
Preferences biosimrc = Preferences.userRoot();
|
||||
String prismCmd = biosimrc.get("biosim.general.prism", "");
|
||||
if (prismCmd.contains("$prism")) {
|
||||
prismCmd = prismCmd.replace("$prism", directory + out + ".prism");
|
||||
} else {
|
||||
prismCmd = prismCmd + " " + directory + out + ".prism";
|
||||
}
|
||||
if (prismCmd.contains("$pctl")) {
|
||||
prismCmd = prismCmd.replace("$pctl", directory + out + ".pctl");
|
||||
} else {
|
||||
prismCmd = prismCmd + " " + directory + out + ".pctl";
|
||||
}
|
||||
message.setLog("Executing:\n" + prismCmd);
|
||||
this.notifyObservers(message);
|
||||
reb2sac = exec.exec(prismCmd, null, work);
|
||||
String error = "", result = "";
|
||||
try {
|
||||
InputStream reb = reb2sac.getInputStream();
|
||||
InputStreamReader isr = new InputStreamReader(reb);
|
||||
BufferedReader br = new BufferedReader(isr);
|
||||
String line;
|
||||
while ((line = br.readLine()) != null) {
|
||||
if (line.startsWith("Result")) {
|
||||
result = line + '\n';
|
||||
}
|
||||
}
|
||||
InputStream reb2 = reb2sac.getErrorStream();
|
||||
int read = reb2.read();
|
||||
while (read != -1) {
|
||||
error += (char) read;
|
||||
read = reb2.read();
|
||||
}
|
||||
br.close();
|
||||
isr.close();
|
||||
reb.close();
|
||||
reb2.close();
|
||||
}
|
||||
catch (Exception e) {
|
||||
// e.printStackTrace();
|
||||
}
|
||||
if (reb2sac != null) {
|
||||
exitValue = reb2sac.waitFor();
|
||||
}
|
||||
if (!error.equals("")) {
|
||||
message.setLog("Errors:\n" + error + "\n");
|
||||
|
||||
this.notifyObservers(message);
|
||||
} else if (!result.equals("")) {
|
||||
message.setLog(result);
|
||||
this.notifyObservers(message);
|
||||
} else {
|
||||
throw new BioSimException("Verification Failed!", "Verification could not be executed. Something went wrong.");
|
||||
}
|
||||
|
||||
exitValue = 0;
|
||||
} else {
|
||||
new File(directory + File.separator + "running").delete();
|
||||
logFile.close();
|
||||
exitValue = 0;
|
||||
}
|
||||
}
|
||||
|
||||
if (reb2sac != null) {
|
||||
exitValue = reb2sac.waitFor();
|
||||
}
|
||||
|
||||
return exitValue;
|
||||
}
|
||||
List<String> keywords = Arrays.asList("A", "bool", "clock", "const", "ctmc", "C", "double", "dtmc", "E", "endinit", "endinvariant", "endmodule",
|
||||
"endobservables", "endrewards", "endsystem", "false", "formula", "filter", "func", "F", "global", "G", "init", "invariant", "I", "int", "label",
|
||||
"max", "mdp", "min", "module", "X", "nondeterministic", "observable", "observables", "of", "Pmax", "Pmin", "P", "pomdp", "popta", "probabilistic",
|
||||
"prob", "pta", "rate", "rewards", "Rmax", "Rmin", "R", "S", "stochastic", "system", "true", "U", "W");
|
||||
|
||||
ArrayList<String> speciesString = new ArrayList<String>();
|
||||
|
||||
*?
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// write pctl file using the SBML constraints
|
||||
/*
|
||||
File file = new File(filename);
|
||||
try {
|
||||
FileWriter out = new FileWriter(file);
|
||||
out.write("ctmc\n");
|
||||
for (String var : LPN.getVariables()) {
|
||||
int i=0;
|
||||
Place place;
|
||||
String lastValue="";
|
||||
while ((place = LPN.getPlace(var+i))!=null) {
|
||||
Transition inTrans = place.getPreset()[0];
|
||||
ExprTree assign = inTrans.getAssignTree(var);
|
||||
lastValue = assign.toString();
|
||||
i++;
|
||||
}
|
||||
Variable variable = LPN.getVariable(var);
|
||||
String initValue = variable.getInitValue();
|
||||
initValue = Long.toString((Math.round(Double.valueOf(initValue))));
|
||||
if (lastValue.equals("")) {
|
||||
out.write("const int "+var+"="+initValue+";\n");
|
||||
} else {
|
||||
out.write("module "+var+"_def\n");
|
||||
out.write(" "+var+" : "+"[0.."+lastValue+"] init "+initValue+";\n");
|
||||
i=0;
|
||||
while ((place = LPN.getPlace(var+i))!=null) {
|
||||
Transition inTrans = place.getPreset()[0];
|
||||
ExprTree assign = inTrans.getAssignTree(var);
|
||||
out.write(" [] "+var+"="+assign.toString()+" -> ");
|
||||
boolean first = true;
|
||||
for (Transition outTrans : place.getPostset()) {
|
||||
assign = outTrans.getAssignTree(var);
|
||||
ExprTree delay = outTrans.getDelayTree();
|
||||
String rate = delay.toString("prism");
|
||||
rate = rate.replace("exponential", "");
|
||||
if (!first) out.write(" + ");
|
||||
out.write(rate+":("+var+"'="+assign.toString()+")");
|
||||
first = false;
|
||||
}
|
||||
out.write(";\n");
|
||||
i++;
|
||||
}
|
||||
out.write("endmodule\n");
|
||||
}
|
||||
for (int i = 0; i < model.getSpeciesCount(); i++)
|
||||
{
|
||||
Species species = model.getSpecies(i);
|
||||
|
||||
if(keywords.contains(species.getId()))
|
||||
{
|
||||
speciesString.add(species.getId());
|
||||
}
|
||||
out.close();
|
||||
for (int i = 0; i < sbml.getModel().getConstraintCount(); i++) {
|
||||
file = new File(filename.replace(".prism", ".pctl"));
|
||||
out = new FileWriter(file);
|
||||
out.write(SBMLutilities.convertMath2PrismProperty(sbml.getModel().getConstraint(i).getMath()));
|
||||
out.close();
|
||||
|
||||
}
|
||||
|
||||
//System.err.println(speciesString);
|
||||
|
||||
for(int i = 0; i < keywords.size(); i++)
|
||||
{
|
||||
if(speciesString.contains(keywords.get(i)))
|
||||
{
|
||||
String Target = " " + keywords.get(i);
|
||||
//System.err.println(Target);
|
||||
math = math.replace(Target, "_" + keywords.get(i));
|
||||
//System.err.println(math);
|
||||
String TargetProperty = "(" + keywords.get(i);
|
||||
math = math.replace(TargetProperty, "(_" + keywords.get(i));
|
||||
}
|
||||
}
|
||||
catch (IOException e) {
|
||||
//TODO: Leandro fix Me
|
||||
//message.setErrorDialog("Error Writing File", "I/O error when writing PRISM file");
|
||||
}
|
||||
*/
|
||||
|
||||
}
|
||||
|
||||
|
||||
return math;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue