1
package dk.aau.cs.io.batchProcessing;
4
import java.io.IOException;
5
import java.util.ArrayList;
6
import java.util.Collection;
7
import java.util.HashMap;
10
import javax.xml.parsers.DocumentBuilder;
11
import javax.xml.parsers.DocumentBuilderFactory;
12
import javax.xml.parsers.ParserConfigurationException;
14
import org.w3c.dom.Document;
15
import org.w3c.dom.Element;
16
import org.w3c.dom.Node;
17
import org.w3c.dom.NodeList;
18
import org.xml.sax.SAXException;
20
import pipe.dataLayer.TAPNQuery;
21
import pipe.dataLayer.TAPNQuery.AlgorithmOption;
22
import pipe.dataLayer.TAPNQuery.ExtrapolationOption;
23
import pipe.dataLayer.TAPNQuery.HashTableSize;
24
import pipe.dataLayer.TAPNQuery.QueryCategory;
25
import pipe.dataLayer.TAPNQuery.SearchOption;
26
import pipe.dataLayer.TAPNQuery.TraceOption;
27
import pipe.gui.widgets.InclusionPlaces;
28
import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
29
import dk.aau.cs.TCTL.TCTLAbstractProperty;
30
import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser;
31
import dk.aau.cs.TCTL.XMLParsing.XMLCTLQueryParser;
32
import dk.aau.cs.TCTL.XMLParsing.XMLQueryParseException;
33
import dk.aau.cs.TCTL.visitors.VerifyPlaceNamesVisitor;
34
import dk.aau.cs.gui.NameGenerator;
35
import dk.aau.cs.io.IdResolver;
36
import dk.aau.cs.io.queries.TAPNQueryLoader;
37
import dk.aau.cs.model.tapn.Constant;
38
import dk.aau.cs.model.tapn.ConstantStore;
39
import dk.aau.cs.model.tapn.IntWeight;
40
import dk.aau.cs.model.tapn.LocalTimedPlace;
41
import dk.aau.cs.model.tapn.SharedPlace;
42
import dk.aau.cs.model.tapn.SharedTransition;
43
import dk.aau.cs.model.tapn.TimeInterval;
44
import dk.aau.cs.model.tapn.TimeInvariant;
45
import dk.aau.cs.model.tapn.TimedArcPetriNet;
46
import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
47
import dk.aau.cs.model.tapn.TimedInhibitorArc;
48
import dk.aau.cs.model.tapn.TimedInputArc;
49
import dk.aau.cs.model.tapn.TimedMarking;
50
import dk.aau.cs.model.tapn.TimedOutputArc;
51
import dk.aau.cs.model.tapn.TimedPlace;
52
import dk.aau.cs.model.tapn.TimedToken;
53
import dk.aau.cs.model.tapn.TimedTransition;
54
import dk.aau.cs.model.tapn.TransportArc;
55
import dk.aau.cs.model.tapn.Weight;
56
import dk.aau.cs.translations.ReductionOption;
57
import dk.aau.cs.util.FormatException;
58
import dk.aau.cs.util.Require;
59
import dk.aau.cs.util.Tuple;
61
public class BatchProcessingLoader {
62
private HashMap<Tuple<TimedTransition, Integer>, TimedPlace> presetArcs;
63
private HashMap<Tuple<TimedTransition, Integer>, TimedPlace> postsetArcs;
64
private HashMap<String, String> placeIDToName;
65
private HashMap<String, String> transitionIDToName;
66
private HashMap<Tuple<TimedTransition, Integer>, TimeInterval> transportArcsTimeIntervals;
68
private IdResolver idResolver = new IdResolver();
70
private NameGenerator nameGenerator = new NameGenerator();
72
public BatchProcessingLoader() {
73
presetArcs = new HashMap<Tuple<TimedTransition,Integer>, TimedPlace>();
74
postsetArcs = new HashMap<Tuple<TimedTransition,Integer>, TimedPlace>();
75
placeIDToName = new HashMap<String, String>();
76
transitionIDToName = new HashMap<String, String>();
77
transportArcsTimeIntervals = new HashMap<Tuple<TimedTransition,Integer>, TimeInterval>();
80
public LoadedBatchProcessingModel load(File file) throws FormatException {
81
Require.that(file != null && file.exists(), "file must be non-null and exist");
83
Document doc = loadDocument(file);
84
if(doc == null) return null;
88
private Document loadDocument(File file) {
90
DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder();
91
return builder.parse(file);
92
} catch (ParserConfigurationException | IOException | SAXException e) {
97
private LoadedBatchProcessingModel parse(Document doc) throws FormatException {
98
ConstantStore constants = new ConstantStore(parseConstants(doc));
100
TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(constants);
102
parseSharedPlaces(doc, network, constants);
103
parseSharedTransitions(doc, network);
105
parseTemplates(doc, network, constants);
106
Collection<TAPNQuery> queries = parseQueries(doc, network);
108
network.buildConstraints();
109
return new LoadedBatchProcessingModel(network, queries);
113
private void parseSharedPlaces(Document doc, TimedArcPetriNetNetwork network, ConstantStore constants) {
114
NodeList sharedPlaceNodes = doc.getElementsByTagName("shared-place");
116
for(int i = 0; i < sharedPlaceNodes.getLength(); i++){
117
Node node = sharedPlaceNodes.item(i);
119
if(node instanceof Element){
120
SharedPlace place = parseSharedPlace((Element)node, network.marking(), constants);
126
private SharedPlace parseSharedPlace(Element element, TimedMarking marking, ConstantStore constants) {
127
String name = element.getAttribute("name");
128
TimeInvariant invariant = TimeInvariant.parse(element.getAttribute("invariant"), constants);
129
int numberOfTokens = Integer.parseInt(element.getAttribute("initialMarking"));
131
if(name.toLowerCase().equals("true") || name.toLowerCase().equals("false")) {
135
SharedPlace place = new SharedPlace(name, invariant);
136
place.setCurrentMarking(marking);
137
for(int j = 0; j < numberOfTokens; j++){
138
marking.add(new TimedToken(place));
143
private void parseSharedTransitions(Document doc, TimedArcPetriNetNetwork network) {
144
NodeList sharedTransitionNodes = doc.getElementsByTagName("shared-transition");
146
for(int i = 0; i < sharedTransitionNodes.getLength(); i++){
147
Node node = sharedTransitionNodes.item(i);
149
if(node instanceof Element){
150
SharedTransition transition = parseSharedTransition((Element)node);
151
network.add(transition);
156
private SharedTransition parseSharedTransition(Element element) {
157
String name = element.getAttribute("name");
159
return new SharedTransition(name);
162
private Collection<TAPNQuery> parseQueries(Document doc, TimedArcPetriNetNetwork network) {
163
Collection<TAPNQuery> queries = new ArrayList<TAPNQuery>();
164
NodeList queryNodes = doc.getElementsByTagName("query");
166
ArrayList<Tuple<String, String>> templatePlaceNames = getPlaceNames(network);
167
for (int i = 0; i < queryNodes.getLength(); i++) {
168
Node q = queryNodes.item(i);
170
if (q instanceof Element) {
171
TAPNQuery query = parseTAPNQuery((Element) q, network);
174
if(!doesPlacesUsedInQueryExist(query, templatePlaceNames)) {
186
private boolean doesPlacesUsedInQueryExist(TAPNQuery query, ArrayList<Tuple<String, String>> templatePlaceNames) {
187
VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames);
189
VerifyPlaceNamesVisitor.Context c = nameChecker.verifyPlaceNames(query.getProperty());
191
return c.getResult();
195
private ArrayList<Tuple<String, String>> getPlaceNames(TimedArcPetriNetNetwork network) {
196
ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
197
for(TimedArcPetriNet tapn : network.allTemplates()) {
198
for(TimedPlace p : tapn.places()) {
199
templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
203
for(TimedPlace p : network.sharedPlaces()) {
204
templatePlaceNames.add(new Tuple<String, String>("", p.name()));
206
return templatePlaceNames;
209
private void parseTemplates(Document doc, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
210
NodeList nets = doc.getElementsByTagName("net");
212
if(nets.getLength() <= 0)
213
throw new FormatException("File did not contain any TAPN components.");
215
for (int i = 0; i < nets.getLength(); i++) {
216
parseTimedArcPetriNet(nets.item(i), network, constants);
220
private List<Constant> parseConstants(Document doc) {
221
List<Constant> constants = new ArrayList<Constant>();
222
NodeList constantNodes = doc.getElementsByTagName("constant");
223
for (int i = 0; i < constantNodes.getLength(); i++) {
224
Node c = constantNodes.item(i);
226
if (c instanceof Element) {
227
Constant constant = parseAndAddConstant((Element) c);
228
constants.add(constant);
234
private void parseTimedArcPetriNet(Node tapnNode, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
235
String name = getTAPNName(tapnNode);
236
boolean active = getActiveStatus(tapnNode);
238
TimedArcPetriNet tapn = new TimedArcPetriNet(name);
239
tapn.setActive(active);
241
nameGenerator.add(tapn);
243
NodeList nodeList = tapnNode.getChildNodes();
244
for (int i = 0; i < nodeList.getLength(); i++) {
245
Node node = nodeList.item(i);
246
if(node instanceof Element){
247
parseElement((Element)node, tapn, network, constants);
252
private boolean getActiveStatus(Node tapnNode) {
253
if (tapnNode instanceof Element) {
254
Element element = (Element)tapnNode;
255
String activeString = element.getAttribute("active");
257
if (activeString == null || activeString.equals(""))
260
return activeString.equals("true");
266
private boolean getInfo(Node tapnNode, String attribute) {
267
Element element = (Element)tapnNode;
268
String string = element.getAttribute(attribute);
269
return string.equals("true");
272
private boolean canGetInfo(Node tapnNode) {
273
if (tapnNode instanceof Element) {
274
Element element = (Element)tapnNode;
275
String timedString = element.getAttribute("timed");
276
String gameString = element.getAttribute("game");
278
if (timedString == null || timedString.equals("") ||
279
gameString == null || gameString.equals("")) {
289
private void parseElement(Element element, TimedArcPetriNet tapn, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
290
if ("place".equals(element.getNodeName())) {
291
parsePlace(element, network, tapn, constants);
292
} else if ("transition".equals(element.getNodeName())) {
293
parseTransition(element, network, tapn);
294
} else if ("arc".equals(element.getNodeName())) {
295
parseAndAddArc(element, tapn, constants);
299
private boolean isNameAllowed(String name) {
300
Require.that(name != null, "name was null");
302
return !name.isEmpty() && java.util.regex.Pattern.matches("[a-zA-Z]([_a-zA-Z0-9])*", name);
306
private String getTAPNName(Node tapnNode) {
307
if (tapnNode instanceof Element) {
308
Element element = (Element)tapnNode;
309
String name = element.getAttribute("name");
311
if (name == null || name.equals(""))
312
name = element.getAttribute("id");
314
if(!isNameAllowed(name)){
315
name = nameGenerator.getNewTemplateName();
317
nameGenerator.updateTemplateIndex(name);
320
return nameGenerator.getNewTemplateName();
324
private void parseTransition(Element transition, TimedArcPetriNetNetwork network, TimedArcPetriNet tapn) {
325
String idInput = transition.getAttribute("id");
326
String nameInput = transition.getAttribute("name");
327
boolean isUrgent = Boolean.parseBoolean(transition.getAttribute("urgent"));
329
idResolver.add(tapn.name(), idInput, nameInput);
331
if (idInput.length() == 0 && nameInput.length() > 0) {
335
if (nameInput.length() == 0 && idInput.length() > 0) {
339
TimedTransition t = new TimedTransition(nameInput);
340
t.setUrgent(isUrgent);
341
if(network.isNameUsedForShared(nameInput)){
342
t.setName(nameGenerator.getNewTransitionName(tapn)); // introduce temporary name to avoid exceptions
344
if(!transitionIDToName.containsKey(idInput))
345
transitionIDToName.put(idInput, nameInput);
346
network.getSharedTransitionByName(nameInput).makeShared(t);
349
transitionIDToName.put(idInput, nameInput);
351
nameGenerator.updateIndicesForAllModels(nameInput);
354
private void parsePlace(Element place, TimedArcPetriNetNetwork network, TimedArcPetriNet tapn, ConstantStore constants) {
355
String idInput = place.getAttribute("id");
356
String nameInput = place.getAttribute("name");
359
int initialMarkingInput = Integer.parseInt(place.getAttribute("initialMarking"));
360
String invariant = place.getAttribute("invariant");
362
if (idInput.length() == 0 && nameInput.length() > 0) {
366
if (nameInput.length() == 0 && idInput.length() > 0) {
370
if(nameInput.toLowerCase().equals("true") || nameInput.toLowerCase().equals("false")) {
371
nameInput = "_" + nameInput;
374
idResolver.add(tapn.name(), idInput, nameInput);
377
if(network.isNameUsedForShared(nameInput)){
378
p = network.getSharedPlaceByName(nameInput);
379
if(!placeIDToName.containsKey(idInput))
380
placeIDToName.put(idInput, nameInput);
383
p = new LocalTimedPlace(nameInput, TimeInvariant.parse(invariant, constants));
385
placeIDToName.put(idInput, nameInput);
386
for (int i = 0; i < initialMarkingInput; i++) {
387
network.marking().add(new TimedToken(p));
390
nameGenerator.updateIndicesForAllModels(nameInput);
393
private void parseAndAddArc(Element arc, TimedArcPetriNet tapn, ConstantStore constants) throws FormatException {
394
String sourceId = idResolver.get(tapn.name(), arc.getAttribute("source"));
395
String targetId = idResolver.get(tapn.name(), arc.getAttribute("target"));
396
String inscription = arc.getAttribute("inscription");
397
String type = arc.getAttribute("type");
400
Weight weight = new IntWeight(1);
401
if(arc.hasAttribute("weight")){
402
weight = Weight.parseWeight(arc.getAttribute("weight"), constants);
406
case "tapnInhibitor":
407
parseAndAddTimedInhibitorArc(sourceId, targetId, inscription, tapn, constants, weight);
410
parseAndAddTimedInputArc(sourceId, targetId, inscription, tapn, constants, weight);
413
parseAndAddTransportArc(sourceId, targetId, inscription, tapn, constants, weight);
416
parseAndAddTimedOutputArc(sourceId, targetId, inscription, tapn, weight);
421
private void parseAndAddTimedOutputArc(String sourceId, String targetId, String inscription, TimedArcPetriNet tapn, Weight weight) throws FormatException {
422
TimedTransition transition = tapn.getTransitionByName(transitionIDToName.get(sourceId));
423
TimedPlace place = tapn.getPlaceByName(placeIDToName.get(targetId));
425
TimedOutputArc outputArc = new TimedOutputArc(transition, place, weight);
427
if(tapn.hasArcFromTransitionToPlace(outputArc.source(),outputArc.destination())) {
428
throw new FormatException("Multiple arcs between a place and a transition is not allowed");
434
private void parseAndAddTransportArc(String sourceId, String targetId, String inscription, TimedArcPetriNet tapn, ConstantStore constants, Weight weight) {
435
String[] inscriptionSplit = {};
436
if (inscription.contains(":")) {
437
inscriptionSplit = inscription.split(":");
439
boolean isInPreSet = false;
440
TimedPlace sourcePlace = null;
441
if(placeIDToName.containsKey(sourceId))
442
sourcePlace = tapn.getPlaceByName(placeIDToName.get(sourceId));
444
if (sourcePlace != null) {
449
TimedTransition transition = tapn.getTransitionByName(transitionIDToName.get(targetId));
450
Tuple<TimedTransition, Integer> hashKey = new Tuple<TimedTransition, Integer>(transition, Integer.parseInt(inscriptionSplit[1]));
452
if (postsetArcs.containsKey(hashKey)) {
453
TimedPlace destPlace = postsetArcs.get(hashKey);
454
TimeInterval interval = TimeInterval.parse(inscriptionSplit[0], constants);
456
assert (sourcePlace != null);
457
assert (transition != null);
458
assert (destPlace != null);
460
TransportArc transArc = new TransportArc(sourcePlace, transition, destPlace, interval, weight);
463
postsetArcs.remove(hashKey);
465
presetArcs.put(hashKey, sourcePlace);
466
transportArcsTimeIntervals.put(hashKey, TimeInterval.parse(inscriptionSplit[0], constants));
469
TimedTransition trans = tapn.getTransitionByName(transitionIDToName.get(sourceId));
470
TimedPlace destPlace = tapn.getPlaceByName(placeIDToName.get(targetId));
471
Tuple<TimedTransition, Integer> hashKey = new Tuple<TimedTransition, Integer>(trans, Integer.parseInt(inscriptionSplit[1]));
473
if (presetArcs.containsKey(hashKey)) {
474
sourcePlace = presetArcs.get(hashKey);
475
TimeInterval interval = transportArcsTimeIntervals.get(hashKey);
477
assert (sourcePlace != null);
478
assert (trans != null);
479
assert (destPlace != null);
481
TransportArc transArc = new TransportArc(sourcePlace, trans, destPlace, interval, weight);
484
presetArcs.remove(hashKey);
485
transportArcsTimeIntervals.remove(hashKey);
487
postsetArcs.put(hashKey, destPlace);
492
private void parseAndAddTimedInputArc(String sourceId, String targetId, String inscription, TimedArcPetriNet tapn, ConstantStore constants, Weight weight) throws FormatException {
493
TimedPlace place = tapn.getPlaceByName(placeIDToName.get(sourceId));
494
TimedTransition transition = tapn.getTransitionByName(transitionIDToName.get(targetId));
495
TimeInterval interval = TimeInterval.parse(inscription, constants);
497
TimedInputArc inputArc = new TimedInputArc(place, transition, interval, weight);
499
if(tapn.hasArcFromPlaceToTransition(inputArc.source(), inputArc.destination())) {
500
throw new FormatException("Multiple arcs between a place and a transition is not allowed");
506
private void parseAndAddTimedInhibitorArc(String sourceId, String targetId, String inscription, TimedArcPetriNet tapn, ConstantStore constants, Weight weight) {
507
TimedPlace place = tapn.getPlaceByName(placeIDToName.get(sourceId));
508
TimedTransition transition = tapn.getTransitionByName(transitionIDToName.get(targetId));
510
TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, TimeInterval.ZERO_INF, weight);
514
private TAPNQuery parseTAPNQuery(Element queryElement, TimedArcPetriNetNetwork network) {
515
String comment = getQueryComment(queryElement);
516
TraceOption traceOption = getQueryTraceOption(queryElement);
517
SearchOption searchOption = getQuerySearchOption(queryElement);
518
HashTableSize hashTableSize = getQueryHashTableSize(queryElement);
519
ExtrapolationOption extrapolationOption = getQueryExtrapolationOption(queryElement);
520
ReductionOption reductionOption = getQueryReductionOption(queryElement);
521
int capacity = Integer.parseInt(queryElement.getAttribute("capacity"));
522
boolean symmetry = getReductionOption(queryElement, "symmetry", true);
523
boolean gcd = getReductionOption(queryElement, "gcd", true);
524
boolean timeDarts = getReductionOption(queryElement, "timeDarts", true);
525
boolean pTrie = getReductionOption(queryElement, "pTrie", true);
526
boolean overApproximation = getReductionOption(queryElement, "overApproximation", false);
527
boolean isOverApproximationEnabled = getApproximationOption(queryElement, "enableOverApproximation", false);
528
boolean isUnderApproximationEnabled = getApproximationOption(queryElement, "enableUnderApproximation", false);
529
int approximationDenominator = getApproximationValue(queryElement, "approximationDenominator", 2);
530
boolean discreteInclusion = getDiscreteInclusionOption(queryElement);
531
boolean active = getActiveStatus(queryElement);
532
InclusionPlaces inclusionPlaces = getInclusionPlaces(queryElement, network);
533
boolean reduction = getReductionOption(queryElement, "reduction", true);
534
String algorithmOption = queryElement.getAttribute("algorithmOption");
535
boolean isCTL = isCTLQuery(queryElement);
536
boolean siphontrap = getReductionOption(queryElement, "useSiphonTrapAnalysis", false);
537
boolean queryReduction = getReductionOption(queryElement, "useQueryReduction", true);
538
boolean stubborn = getReductionOption(queryElement, "useStubbornReduction", true);
540
TCTLAbstractProperty query;
541
if (queryElement.getElementsByTagName("formula").item(0) != null){
542
query = parseCTLQueryProperty(queryElement);
544
query = parseQueryProperty(queryElement.getAttribute("query"));
548
TAPNQuery parsedQuery = new TAPNQuery(comment, capacity, query, traceOption, searchOption, reductionOption, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, hashTableSize, extrapolationOption, inclusionPlaces, isOverApproximationEnabled, isUnderApproximationEnabled, approximationDenominator);
549
parsedQuery.setActive(active);
550
parsedQuery.setDiscreteInclusion(discreteInclusion);
551
parsedQuery.setCategory(TAPNQueryLoader.detectCategory(query, isCTL));
552
parsedQuery.setUseSiphontrap(siphontrap);
553
parsedQuery.setUseQueryReduction(queryReduction);
554
parsedQuery.setUseStubbornReduction(stubborn);
555
if (parsedQuery.getCategory() == QueryCategory.CTL && algorithmOption != null){
556
parsedQuery.setAlgorithmOption(AlgorithmOption.valueOf(algorithmOption));
557
// RenameTemplateVisitor rt = new RenameTemplateVisitor("",
558
// network.activeTemplates().get(0).name());
559
// parsedQuery.getProperty().accept(rt, null);
566
private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
568
if(!queryElement.hasAttribute(attributeName)){
573
result = Integer.parseInt(queryElement.getAttribute(attributeName));
574
} catch(Exception e) {
575
result = defaultValue;
580
private boolean getApproximationOption(Element queryElement, String attributeName, boolean defaultValue)
582
if(!queryElement.hasAttribute(attributeName)){
587
result = queryElement.getAttribute(attributeName).equals("true");
588
} catch(Exception e) {
589
result = defaultValue;
594
private boolean getDiscreteInclusionOption(Element queryElement) {
595
boolean discreteInclusion;
597
discreteInclusion = queryElement.getAttribute("discreteInclusion").equals("true");
598
} catch(Exception e) {
599
discreteInclusion = false;
601
return discreteInclusion;
604
private InclusionPlaces getInclusionPlaces(Element queryElement, TimedArcPetriNetNetwork network) {
605
List<TimedPlace> places = new ArrayList<TimedPlace>();
607
String inclusionPlaces;
609
inclusionPlaces = queryElement.getAttribute("inclusionPlaces");
610
} catch(Exception e) {
611
inclusionPlaces = "*ALL*";
614
if(!queryElement.hasAttribute("inclusionPlaces") || inclusionPlaces.equals("*ALL*"))
615
return new InclusionPlaces();
617
if(inclusionPlaces.isEmpty() || inclusionPlaces.equals("*NONE*"))
618
return new InclusionPlaces(InclusionPlacesOption.UserSpecified, new ArrayList<TimedPlace>());
621
String[] placeNames = inclusionPlaces.split(",");
623
for(String name : placeNames) {
624
if(name.contains(".")) {
625
String templateName = name.split("\\.")[0];
626
String placeName = name.split("\\.")[1];
628
// "true" and "false" are reserved keywords and places using these names are renamed to "_true" and "_false" respectively
629
if(placeName.equalsIgnoreCase("false") || placeName.equalsIgnoreCase("true"))
630
placeName = "_" + placeName;
632
TimedPlace p = network.getTAPNByName(templateName).getPlaceByName(placeName);
634
} else { // shared Place
636
if(name.equalsIgnoreCase("false") || name.equalsIgnoreCase("true"))
639
TimedPlace p = network.getSharedPlaceByName(name);
644
return new InclusionPlaces(InclusionPlacesOption.UserSpecified, places);
647
private boolean isCTLQuery(Element queryElement) {
648
if(!queryElement.hasAttribute("type")){
653
result = queryElement.getAttribute("type").equals("CTL");
654
} catch(Exception e) {
660
private boolean getReductionOption(Element queryElement, String attributeName, boolean defaultValue) {
663
result = queryElement.getAttribute(attributeName).equals("true");
664
} catch(Exception e) {
665
result = defaultValue;
670
private TCTLAbstractProperty parseCTLQueryProperty(Node queryElement){
671
TCTLAbstractProperty query = null;
674
query = XMLCTLQueryParser.parse(queryElement);
675
} catch (XMLQueryParseException e) {
676
System.err.println("No query was specified: " + e.getStackTrace().toString());
682
private TCTLAbstractProperty parseQueryProperty(String queryToParse) {
683
TCTLAbstractProperty query = null;
686
query = TAPAALQueryParser.parse(queryToParse);
687
} catch (Exception e) {
688
System.err.println("No query was specified: " + e.getStackTrace().toString());
693
private ReductionOption getQueryReductionOption(Element queryElement) {
694
ReductionOption reductionOption;
696
reductionOption = ReductionOption.valueOf(queryElement.getAttribute("reductionOption"));
697
} catch (Exception e) {
698
reductionOption = ReductionOption.VerifyTAPN;
700
return reductionOption;
703
private ExtrapolationOption getQueryExtrapolationOption(Element queryElement) {
704
ExtrapolationOption extrapolationOption;
706
extrapolationOption = ExtrapolationOption.valueOf(queryElement.getAttribute("extrapolationOption"));
707
} catch (Exception e) {
708
extrapolationOption = ExtrapolationOption.AUTOMATIC;
710
return extrapolationOption;
713
private HashTableSize getQueryHashTableSize(Element queryElement) {
714
HashTableSize hashTableSize;
716
hashTableSize = HashTableSize.valueOf(queryElement.getAttribute("hashTableSize"));
717
} catch (Exception e) {
718
hashTableSize = HashTableSize.MB_16;
720
return hashTableSize;
723
private SearchOption getQuerySearchOption(Element queryElement) {
724
SearchOption searchOption;
726
searchOption = SearchOption.valueOf(queryElement.getAttribute("searchOption"));
727
} catch (Exception e) {
728
searchOption = SearchOption.BFS;
733
private TraceOption getQueryTraceOption(Element queryElement) {
734
TraceOption traceOption;
736
traceOption = TraceOption.valueOf(queryElement.getAttribute("traceOption"));
737
} catch (Exception e) {
738
traceOption = TraceOption.NONE;
743
private String getQueryComment(Element queryElement) {
746
comment = queryElement.getAttribute("name");
747
} catch (Exception e) {
748
comment = "No comment specified";
753
private Constant parseAndAddConstant(Element constantElement) {
754
String name = constantElement.getAttribute("name");
755
int value = Integer.parseInt(constantElement.getAttribute("value"));
757
return new Constant(name, value);
added
removed
src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java
