Skip to content
Permalink
Browse files

TLCModelLaunchDataProvider's zero coverage never resets - #323

- Zero coverage is now reset between runs; architectural notes left in comments.

#323
[Bug][[Toolbox]
  • Loading branch information...
quaeler committed Oct 4, 2019
1 parent 16128ff commit ea181430c9154bc518a49b6739d313db2d6b1e8f
@@ -201,6 +201,7 @@ protected void initialize()
userOutput = new Document(NO_OUTPUT_AVAILABLE);
constantExprEvalOutput = "";
isSymmetryWithLiveness = false;
zeroCoverage = false;
}

/**
@@ -473,15 +474,15 @@ public void onOutput(ITypedRegion region, String text)
CoverageInformationItem item = CoverageInformationItem.parseCost(outputMessage, getModelName());
this.coverageInfo.add(item);
if (item.getCount() == 0) {
this.zeroCoverage = true;
zeroCoverage = true;
}
informPresenter(ITLCModelLaunchDataPresenter.COVERAGE);
break;
case EC.TLC_COVERAGE_VALUE:
item = CoverageInformationItem.parse(outputMessage, getModelName());
this.coverageInfo.add(item);
if (item.getCount() == 0) {
this.zeroCoverage = true;
zeroCoverage = true;
}
informPresenter(ITLCModelLaunchDataPresenter.COVERAGE);
break;
@@ -1009,7 +1010,7 @@ public CoverageInformation getCoverageInfo()
}

public boolean hasZeroCoverage() {
return this.zeroCoverage;
return zeroCoverage;
}

public List<StateSpaceInformationItem> getProgressInformation()
@@ -231,7 +231,14 @@ public synchronized void disconnect(ITLCOutputListener listener)
}

/**
* Retrieves the data provider for the given configuration
* Retrieves the data provider for the given configuration.
*
* Architecture TODO: it is unclear what we are gaining by keeping the same instance of a launch data provider
* attached to an instance of Model for the lifespan of the app (except in the following cases:
* . the model is deleted
* . loading existing output from the filesystem for the model
* )
*
* @return a data provider for the current model
*/
public synchronized TLCModelLaunchDataProvider getProvider(Model model)

0 comments on commit ea18143

Please sign in to comment.
You can’t perform that action at this time.