From 0667019a053bc5667f8cebfa535482b6d6a51af8 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 26 Aug 2016 06:29:30 +0000 Subject: [PATCH] explicit: Make calls to StateModelChecker.loadLabelsFile static git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11747 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 2 +- prism/src/explicit/CTMDPModelChecker.java | 2 +- prism/src/explicit/DTMCModelChecker.java | 2 +- prism/src/explicit/MDPModelChecker.java | 2 +- prism/src/explicit/PrismSTPGAbstractRefine.java | 3 ++- prism/src/explicit/STPGModelChecker.java | 2 +- 6 files changed, 7 insertions(+), 6 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 51917514..ff7f36dc 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -935,7 +935,7 @@ public class CTMCModelChecker extends ProbModelChecker ctmc.buildFromPrismExplicit(args[0]); ctmc.addInitialState(0); //System.out.println(ctmc); - labels = mc.loadLabelsFile(args[1]); + labels = StateModelChecker.loadLabelsFile(args[1]); //System.out.println(labels); target = labels.get(args[2]); if (target == null) diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index 53a973ac..e49accfc 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -286,7 +286,7 @@ public class CTMDPModelChecker extends ProbModelChecker ctmdp.buildFromPrismExplicit(args[0]); ctmdp.addInitialState(0); System.out.println(ctmdp); - labels = mc.loadLabelsFile(args[1]); + labels = StateModelChecker.loadLabelsFile(args[1]); System.out.println(labels); target = labels.get(args[2]); if (target == null) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index d72741f4..28cc2cf6 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -1624,7 +1624,7 @@ public class DTMCModelChecker extends ProbModelChecker dtmc.buildFromPrismExplicit(args[0]); dtmc.addInitialState(0); //System.out.println(dtmc); - Map labels = mc.loadLabelsFile(args[1]); + Map labels = StateModelChecker.loadLabelsFile(args[1]); //System.out.println(labels); BitSet target = labels.get(args[2]); if (target == null) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index edec0848..b2b1e183 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -1756,7 +1756,7 @@ public class MDPModelChecker extends ProbModelChecker mdp.buildFromPrismExplicit(args[0]); mdp.addInitialState(0); //System.out.println(mdp); - labels = mc.loadLabelsFile(args[1]); + labels = StateModelChecker.loadLabelsFile(args[1]); //System.out.println(labels); init = labels.get("init"); target = labels.get(args[2]); diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 88a3ace6..02ba0805 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/prism/src/explicit/PrismSTPGAbstractRefine.java @@ -116,8 +116,9 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine } } + new StateModelChecker(null); // Get initial/target (concrete) states - labels = new StateModelChecker(null).loadLabelsFile(labFile); + labels = StateModelChecker.loadLabelsFile(labFile); initialConcrete = labels.get("init"); targetConcrete = labels.get(targetLabel); if (targetConcrete == null) diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index b5fce8d8..2e1bc463 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -920,7 +920,7 @@ public class STPGModelChecker extends ProbModelChecker stpg.buildFromPrismExplicit(args[0]); stpg.addInitialState(0); //System.out.println(stpg); - labels = mc.loadLabelsFile(args[1]); + labels = StateModelChecker.loadLabelsFile(args[1]); //System.out.println(labels); target = labels.get(args[2]); if (target == null)