Browse Source

ExportIterations: Log the file name when exporting iterations

master
Joachim Klein 8 years ago
parent
commit
29e2ba21eb
  1. 6
      prism/src/explicit/DTMCModelChecker.java
  2. 4
      prism/src/explicit/MDPModelChecker.java
  3. 1
      prism/src/mtbdd/PM_JOR.cc
  4. 1
      prism/src/mtbdd/PM_JORInterval.cc
  5. 1
      prism/src/mtbdd/PM_Power.cc
  6. 1
      prism/src/mtbdd/PM_PowerInterval.cc

6
prism/src/explicit/DTMCModelChecker.java

@ -1017,6 +1017,7 @@ public class DTMCModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachProbs value iteration (" + description + ")"); iterationsExport = new ExportIterations("Explicit DTMC ReachProbs value iteration (" + description + ")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -1144,6 +1145,7 @@ public class DTMCModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachProbs interval iteration (" + description + ")"); iterationsExport = new ExportIterations("Explicit DTMC ReachProbs interval iteration (" + description + ")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -1861,6 +1863,7 @@ public class DTMCModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachRewards value iteration"); iterationsExport = new ExportIterations("Explicit DTMC ReachRewards value iteration");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -1964,6 +1967,7 @@ public class DTMCModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachRewards value iteration (" + description + ")"); iterationsExport = new ExportIterations("Explicit DTMC ReachRewards value iteration (" + description + ")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -2073,6 +2077,7 @@ public class DTMCModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachRewards interval iteration (" + description + ") ..."); iterationsExport = new ExportIterations("Explicit DTMC ReachRewards interval iteration (" + description + ") ...");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Create solution vector(s) // Create solution vector(s)
@ -2369,6 +2374,7 @@ public class DTMCModelChecker extends ProbModelChecker
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = ExportIterations.createWithUniqueFilename("Explicit DTMC BSCC steady state value iteration", "iterations-ss-bscc"); iterationsExport = ExportIterations.createWithUniqueFilename("Explicit DTMC BSCC steady state value iteration", "iterations-ss-bscc");
iterationsExport.exportVector(soln); iterationsExport.exportVector(soln);
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Start iterations // Start iterations

4
prism/src/explicit/MDPModelChecker.java

@ -837,6 +837,7 @@ public class MDPModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit MDP ReachProbs value iteration (" + description + ")"); iterationsExport = new ExportIterations("Explicit MDP ReachProbs value iteration (" + description + ")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -926,6 +927,7 @@ public class MDPModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit MDP ReachProbs interval iteration (" + description + ")"); iterationsExport = new ExportIterations("Explicit MDP ReachProbs interval iteration (" + description + ")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -2305,6 +2307,7 @@ public class MDPModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit MDP ReachRewards value iteration (" + description +")"); iterationsExport = new ExportIterations("Explicit MDP ReachRewards value iteration (" + description +")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Store num states // Store num states
@ -2450,6 +2453,7 @@ public class MDPModelChecker extends ProbModelChecker
ExportIterations iterationsExport = null; ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit MDP ReachRewards interval iteration (" + description + ")"); iterationsExport = new ExportIterations("Explicit MDP ReachRewards interval iteration (" + description + ")");
mainLog.println("Exporting iterations to " + iterationsExport.getFileName());
} }
// Create initial solution vector(s) // Create initial solution vector(s)

1
prism/src/mtbdd/PM_JOR.cc

@ -131,6 +131,7 @@ jdouble omega // omega (jor parameter)
title += ")"; title += ")";
iterationExport.reset(new ExportIterations(title.c_str())); iterationExport.reset(new ExportIterations(title.c_str()));
PM_PrintToMainLog(env, "Exporting iterations to %s\n", iterationExport->getFileName().c_str());
iterationExport->exportVector(sol, (transpose?cvars:rvars), num_rvars, odd, 0); iterationExport->exportVector(sol, (transpose?cvars:rvars), num_rvars, odd, 0);
} }

1
prism/src/mtbdd/PM_JORInterval.cc

@ -146,6 +146,7 @@ jint flags
title += "), interval"; title += "), interval";
iterationExport.reset(new ExportIterations(title.c_str())); iterationExport.reset(new ExportIterations(title.c_str()));
PM_PrintToMainLog(env, "Exporting iterations to %s\n", iterationExport->getFileName().c_str());
iterationExport->exportVector(sol_below, (transpose?cvars:rvars), num_rvars, odd, 0); iterationExport->exportVector(sol_below, (transpose?cvars:rvars), num_rvars, odd, 0);
iterationExport->exportVector(sol_above, (transpose?cvars:rvars), num_rvars, odd, 1); iterationExport->exportVector(sol_above, (transpose?cvars:rvars), num_rvars, odd, 1);
} }

1
prism/src/mtbdd/PM_Power.cc

@ -100,6 +100,7 @@ jboolean transpose // transpose A? (i.e. solve xA=b not Ax=b?)
std::unique_ptr<ExportIterations> iterationExport; std::unique_ptr<ExportIterations> iterationExport;
if (PM_GetFlagExportIterations()) { if (PM_GetFlagExportIterations()) {
iterationExport.reset(new ExportIterations("PM_Power")); iterationExport.reset(new ExportIterations("PM_Power"));
PM_PrintToMainLog(env, "Exporting iterations to %s\n", iterationExport->getFileName().c_str());
iterationExport->exportVector(sol, (transpose?cvars:rvars), num_rvars, odd, 0); iterationExport->exportVector(sol, (transpose?cvars:rvars), num_rvars, odd, 0);
} }

1
prism/src/mtbdd/PM_PowerInterval.cc

@ -110,6 +110,7 @@ jint flags
std::unique_ptr<ExportIterations> iterationExport; std::unique_ptr<ExportIterations> iterationExport;
if (PM_GetFlagExportIterations()) { if (PM_GetFlagExportIterations()) {
iterationExport.reset(new ExportIterations("PM_Power (interval)")); iterationExport.reset(new ExportIterations("PM_Power (interval)"));
PM_PrintToMainLog(env, "Exporting iterations to %s\n", iterationExport->getFileName().c_str());
iterationExport->exportVector(sol_below, (transpose?cvars:rvars), num_rvars, odd, 0); iterationExport->exportVector(sol_below, (transpose?cvars:rvars), num_rvars, odd, 0);
iterationExport->exportVector(sol_above, (transpose?cvars:rvars), num_rvars, odd, 1); iterationExport->exportVector(sol_above, (transpose?cvars:rvars), num_rvars, odd, 1);
} }

Loading…
Cancel
Save