Browse Source

Code tidy.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10815 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
commit
ff05caf158
  1. 2
      prism/src/parser/PrismParser.java
  2. 8
      prism/src/prism/NondetModel.java
  3. 6
      prism/src/simulator/GenerateSimulationPath.java
  4. 1
      prism/src/sparse/PS_NondetMultiObj.cc
  5. 1
      prism/src/sparse/PS_NondetMultiObjGS.cc
  6. 6
      prism/src/sparse/PS_NondetReachReward.cc
  7. 3
      prism/src/sparse/PS_NondetUntil.cc
  8. 8
      prism/src/userinterface/model/GUIMultiModelHandler.java

2
prism/src/parser/PrismParser.java

@ -136,6 +136,8 @@ public class PrismParser implements PrismParserConstants {
public ModulesFile parseModulesFile(InputStream str, ModelType typeOverride) throws PrismLangException
{
new Exception().printStackTrace(System.out);
ModulesFile mf = null;
// (Re)start parser

8
prism/src/prism/NondetModel.java

@ -384,6 +384,14 @@ public class NondetModel extends ProbModel
} else {
PrismSparse.ExportMDP(trans, transActions, getSynchs(), getTransSymbol(), allDDRowVars, allDDColVars, allDDNondetVars, odd, exportType,
(file != null) ? file.getPath() : null);
if (exportType == Prism.EXPORT_DOT_STATES) {
PrismLog tmpLog;
tmpLog = PrismFileLog.create(file.getPath(), true);
// insert states info into dot file
getReachableStates().printDot(tmpLog);
// print footer
tmpLog.println("}");
}
}
}

6
prism/src/simulator/GenerateSimulationPath.java

@ -341,7 +341,7 @@ public class GenerateSimulationPath
private PathDisplayer generateDisplayerForExport() throws PrismException
{
PrismLog log;
PathToText displayer;
PathToDaikonTrace displayer;
if (file != null) {
log = new PrismFileLog(file.getPath());
@ -351,8 +351,8 @@ public class GenerateSimulationPath
} else {
log = mainLog;
}
displayer = new PathToText(log, modulesFile);
displayer.setColSep(simPathSep);
displayer = new PathToDaikonTrace(log, modulesFile);
//displayer.setColSep(simPathSep);
displayer.setVarsToShow(simVars);
displayer.setShowProbs(simPathShowProbs);
displayer.setShowRewards(simPathShowRewards);

1
prism/src/sparse/PS_NondetMultiObj.cc

@ -94,7 +94,6 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
double time_taken, time_for_setup, time_for_iters;
// adversary stuff
int export_adv_enabled = export_adv;
bool adv_loop = false;
FILE *fp_adv = NULL;
int adv_j;
int *adv = NULL;

1
prism/src/sparse/PS_NondetMultiObjGS.cc

@ -94,7 +94,6 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
double time_taken, time_for_setup, time_for_iters;
// adversary stuff
int export_adv_enabled = export_adv;
bool adv_loop = false;
FILE *fp_adv = NULL;
int adv_j;
//int *adv = NULL;

6
prism/src/sparse/PS_NondetReachReward.cc

@ -90,10 +90,8 @@ jboolean min // min or max probabilities (true = min, false = max)
double time_taken, time_for_setup, time_for_iters;
// adversary stuff
int export_adv_enabled = export_adv;
bool adv_loop = false;
FILE *fp_adv = NULL;
int adv_j;
bool adv_new;
int *adv = NULL;
// action info
jstring *action_names_jstrings;
@ -266,7 +264,6 @@ jboolean min // min or max probabilities (true = min, false = max)
for (i = 0; i < n; i++) {
d1 = 0.0; // initial value doesn't matter
first = true; // (because we also remember 'first')
adv_new = false;
// get pointers to nondeterministic choices for state i
if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
else { l1 = h1; h1 += row_counts[i]; }
@ -340,9 +337,6 @@ jboolean min // min or max probabilities (true = min, false = max)
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// if we're done, but adversary generation is required, go round once more
if (done && adv) adv_loop = !adv_loop;
}
// Traverse matrix to extract adversary

3
prism/src/sparse/PS_NondetUntil.cc

@ -86,10 +86,8 @@ jlong _strat // strategy storage
double time_taken, time_for_setup, time_for_iters;
// adversary stuff
int export_adv_enabled = export_adv;
bool adv_loop = false;
FILE *fp_adv = NULL;
int adv_j;
bool adv_new;
int *adv = NULL;
// action info
jstring *action_names_jstrings;
@ -239,7 +237,6 @@ jlong _strat // strategy storage
for (i = 0; i < n; i++) {
d1 = 0.0; // initial value doesn't matter
first = true; // (because we also remember 'first')
adv_new = false;
if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
else { l1 = h1; h1 += row_counts[i]; }
for (j = l1; j < h1; j++) {

8
prism/src/userinterface/model/GUIMultiModelHandler.java

@ -533,6 +533,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
{
tree.stopParsing();
parsing = false;
System.out.println("parsing = false");
parsedModel = m;
modifiedSinceParse = false;
lastError = "Parse Successful";
@ -548,6 +549,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
waiter.interrupt();
}
int parseDelay = theModel.getPrism().getSettings().getInteger(PrismSettings.MODEL_PARSE_DELAY);
System.out.println("*");
waiter = new WaitParseThread(parseDelay, this);
waiter.start();
//Funky thread waiting stuff
@ -944,6 +946,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
// If the flag has just been switched ON, do a parse...
if (autoParse) {
System.out.println("## " + parsing);
tree.makeNotUpToDate();
theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE));
if (!parsing) {
@ -956,6 +959,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
waiter.start();
}
} else {
System.out.println("**");
parseAfterParse = true;
}
theModel.doEnables();
@ -1210,6 +1214,9 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
public WaitParseThread(int time, GUIMultiModelHandler handler)
{
new Exception().printStackTrace(System.out);
this.time = time;
this.handler = handler;
}
@ -1218,6 +1225,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
{
try {
sleep(time);
System.out.println(time);
parseThread = new ParseModelThread(handler, editor.getParseText(), currentMode == PEPA_MODE, isAutoParse());
parsing = true;
tree.startParsing();

Loading…
Cancel
Save