From a4734bf7a609c151e364498ea58d0f9aa93b58f2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 1 Jun 2019 17:00:15 +0100 Subject: [PATCH] Basic auto-detection of model type for explicit file import. --- .../import/dice.pm.importexport.auto | 1 + .../import/poll2.sm.importexport.auto | 1 + .../import/robot.prism.importexport.auto | 1 + prism/src/prism/ExplicitFiles2ModelInfo.java | 75 ++++++++++++++++++- prism/src/prism/Prism.java | 2 +- prism/src/prism/PrismCL.java | 4 +- 6 files changed, 77 insertions(+), 7 deletions(-) diff --git a/prism-tests/functionality/import/dice.pm.importexport.auto b/prism-tests/functionality/import/dice.pm.importexport.auto index e1f260dc..5ff4cd07 100644 --- a/prism-tests/functionality/import/dice.pm.importexport.auto +++ b/prism-tests/functionality/import/dice.pm.importexport.auto @@ -1,2 +1,3 @@ -dtmc -importmodel dice.all -exportmodel dice.sta,tra,lab,srew -dtmc -importmodel dice.all -exportmodel dice.sta,tra,lab -ex +-importmodel dice.all -exportmodel dice.sta,tra,lab -ex diff --git a/prism-tests/functionality/import/poll2.sm.importexport.auto b/prism-tests/functionality/import/poll2.sm.importexport.auto index 3b427a4c..45d9e506 100644 --- a/prism-tests/functionality/import/poll2.sm.importexport.auto +++ b/prism-tests/functionality/import/poll2.sm.importexport.auto @@ -1,2 +1,3 @@ -ctmc -importmodel poll2.all -exportmodel poll2.sta,tra,lab,srew -ctmc -importmodel poll2.all -exportmodel poll2.sta,tra,lab -ex +-importmodel poll2.all -exportmodel poll2.sta,tra,lab -ex diff --git a/prism-tests/functionality/import/robot.prism.importexport.auto b/prism-tests/functionality/import/robot.prism.importexport.auto index 14ef2afa..f2451568 100644 --- a/prism-tests/functionality/import/robot.prism.importexport.auto +++ b/prism-tests/functionality/import/robot.prism.importexport.auto @@ -1,2 +1,3 @@ -mdp -importmodel robot.all -exportmodel robot.sta,tra,lab,srew -mdp -importmodel robot.all -exportmodel robot.sta,tra,lab -ex +-importmodel robot.all -exportmodel robot.sta,tra,lab -ex diff --git a/prism/src/prism/ExplicitFiles2ModelInfo.java b/prism/src/prism/ExplicitFiles2ModelInfo.java index d1080e4c..7422f454 100644 --- a/prism/src/prism/ExplicitFiles2ModelInfo.java +++ b/prism/src/prism/ExplicitFiles2ModelInfo.java @@ -81,11 +81,13 @@ public class ExplicitFiles2ModelInfo extends PrismComponent /** * Build a ModelInfo object corresponding to the passed in states/transitions/labels files. - * If {@code typeOverride} is null, we assume model is an MDP. + * If {@code typeOverride} is provided, this is used as the model type; + * if it is null, we try to auto-detect it (or default to MDP if that cannot be done). * * @param statesFile states file (may be {@code null}) * @param transFile transitions file * @param labelsFile labels file (may be {@code null}) + * @param typeOverride model type (auto-detected if {@code null}) */ public ModelInfo buildModelInfo(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException { @@ -102,8 +104,21 @@ public class ExplicitFiles2ModelInfo extends PrismComponent extractLabelNamesFromLabelsFile(labelsFile); } - // Set model type: if no preference stated, assume default of MDP - ModelType modelType = (typeOverride == null) ? ModelType.MDP : typeOverride; + // Set model type: if no preference stated, try to autodetect + ModelType modelType; + if (typeOverride == null) { + ModelType typeAutodetect = autodetectModelType(transFile); + if (typeAutodetect != null) { + mainLog.println("Auto-detected model type: " + typeAutodetect); + } else { + typeAutodetect = ModelType.MDP; + mainLog.println("Assuming default model type: " + typeAutodetect); + } + modelType = typeAutodetect; + } else { + mainLog.println("Using specified model type: " + typeOverride); + modelType = typeOverride; + } // Create and return ModelInfo object with above info ModelInfo modelInfo = new ModelInfo() @@ -335,4 +350,58 @@ public class ExplicitFiles2ModelInfo extends PrismComponent throw new PrismException("File I/O error reading from \"" + labelsFile + "\""); } } + + /** + * Autodetect the model type based on a sample of the lines from a transitions file. + * If not possible, return null; + * @param transFile transitions file + */ + private ModelType autodetectModelType(File transFile) + { + String s, ss[]; + + // Open file for reading, automatic close when done + try (BufferedReader in = new BufferedReader(new FileReader(transFile))) { + // Look at first line + s = in.readLine(); + if (s == null) { + return null; + } + ss = s.trim().split(" "); + // 3 parts - should be an MDP + if (ss.length == 3) { + return ModelType.MDP; + } + // Not 2 parts: error; give up + else if (ss.length != 2) { + return null; + } + // Now choose between DTMC and CTMC + // Read up to max remaining lines + int lines = 0; + int max = 5; + s = in.readLine(); + while (s != null && lines < max) { + lines++; + ss = s.trim().split(" "); + // Look at probability/rate + double d = Double.parseDouble(ss[2]); + // Looks like a rate: guess CTMC + if (d > 1) { + return ModelType.CTMC; + } + // All non-rates so far: guess DTMC + if (lines == max) { + return ModelType.DTMC; + } + // Read next line + s = in.readLine(); + } + return null; + } catch (NumberFormatException e) { + return null; + } catch (IOException e) { + return null; + } + } } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index e04b2cca..2b08c89a 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1921,7 +1921,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener * @param transFile File containing the list of transitions (required) * @param labelsFile File containing label definitions (optional, can be null) * @param stateRewardsFile File containing state reward definitions (optional, can be null) - * @param typeOverride Type of model to be built (optional, use null if not required) + * @param typeOverride Model type (auto-detected if {@code null}) */ public void loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelType typeOverride) throws PrismException { diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 5abda65d..ab796200 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -602,9 +602,7 @@ public class PrismCL implements PrismModelListener modulesFile = prism.importPrismPreprocFile(new File(modelFilename), prismppParamsList); prism.loadPRISMModel(modulesFile); } else if (importtrans) { - mainLog.print("\nImporting model ("); - mainLog.print(typeOverride == null ? "MDP" : typeOverride); - mainLog.print(") from \"" + modelFilename + "\""); + mainLog.print("\nImporting model from \"" + modelFilename + "\""); if (importstates) { mainLog.print(", \"" + importStatesFilename + "\""); sf = new File(importStatesFilename);