Browse Source

Bugfix: Model labels get exported twice when there is also a properties file due to recent ModelInfo refacetoring.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11984 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 9 years ago
parent
commit
32404e1ab6
  1. 5
      prism/src/prism/Prism.java

5
prism/src/prism/Prism.java

@ -2705,8 +2705,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
List<String> labelNames = new ArrayList<String>();
labelNames.add("init");
labelNames.add("deadlock");
labelNames.addAll(currentModelInfo.getLabelNames());
if (propertiesFile != null) {
if (propertiesFile == null) {
labelNames.addAll(currentModelInfo.getLabelNames());
} else {
LabelList ll = propertiesFile.getCombinedLabelList();
int numLabels = ll.size();
for (int i = 0; i < numLabels; i++) {

Loading…
Cancel
Save