~tapaal-contributor/tapaal/disappearing-tokens-1940098

private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL encountered an error trying to parse one or more of the queries in the model.\n\nThe queries that could not be parsed will not show up in the query list.";

private HashMap<TimedTransitionComponent, TransportArcComponent> presetArcs;

private HashMap<TimedTransitionComponent, TransportArcComponent> postsetArcs;

private HashMap<TransportArcComponent, TimeInterval> transportArcsTimeIntervals;

private TimedArcPetriNet tapn;

private DataLayer guiModel;

private ArrayList<TAPNQuery> queries;

private TreeMap<String, Constant> constants;

private DrawingSurfaceImpl drawingSurface;

private NameGenerator nameGenerator = new NameGenerator();

private boolean firstQueryParsingWarning = true;

private boolean firstInhibitorIntervalWarning = true;

public TapnLegacyXmlLoader(DrawingSurfaceImpl drawingSurfaceImpl) {

presetArcs = new HashMap<TimedTransitionComponent, TransportArcComponent>();

postsetArcs = new HashMap<TimedTransitionComponent, TransportArcComponent>();

transportArcsTimeIntervals = new HashMap<TransportArcComponent, TimeInterval>();

queries = new ArrayList<TAPNQuery>();

100

constants = new TreeMap<String, Constant>();

101

this.drawingSurface = drawingSurfaceImpl;

102

}

103

104

public LoadedModel load(File file) throws FormatException {

105

Require.that(file != null && file.exists(), "file must be non-null and exist");

106

107

Document doc = loadDocument(file);

108

if(doc == null) return null;

109

return parse(doc);

110

}

111

112

private Document loadDocument(File file) {

113

try {

114

DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder();

115

return builder.parse(file);

116

} catch (ParserConfigurationException e) {

117

return null;

118

} catch (SAXException e) {

119

return null;

120

} catch (IOException e) {

121

return null;

122

}

123

}

124

125

private LoadedModel parse(Document tapnDoc) throws FormatException {

126

ArrayList<Template> templates = new ArrayList<Template>();

127

128

NodeList constantNodes = tapnDoc.getElementsByTagName("constant");

129

for (int i = 0; i < constantNodes.getLength(); i++) {

130

Node c = constantNodes.item(i);

131

132

if (c instanceof Element) {

133

parseAndAddConstant((Element) c);

134

}

135

}

136

137

TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(new ConstantStore(constants.values()));

138

NodeList nets = tapnDoc.getElementsByTagName("net");

139

140

if(nets.getLength() <= 0)

141

throw new FormatException("File did not contain any TAPN components.");

142

143

templates.add(parseTimedArcPetriNetAsOldFormat(nets.item(0), network));

144

145

checkThatQueriesUseExistingPlaces(network);

146

147

return new LoadedModel(network, templates, queries);

148

}

149

150

private void checkThatQueriesUseExistingPlaces(TimedArcPetriNetNetwork network) {

151

ArrayList<TAPNQuery> okQueries = new ArrayList<TAPNQuery>();

152

ArrayList<Tuple<String,String>> templatePlaceNames = getTemplatePlaceNames(network);

153

for(TAPNQuery query : queries) {

154

if(!doesPlacesUsedInQueryExist(query, templatePlaceNames)) {

155

if(firstQueryParsingWarning) {

156

JOptionPane.showMessageDialog(CreateGui.getApp(), ERROR_PARSING_QUERY_MESSAGE, "Error Parsing Query", JOptionPane.ERROR_MESSAGE);

157

firstQueryParsingWarning = false;

158

}

159

continue;

160

}

161

162

okQueries.add(query);

163

}

164

165

queries = okQueries;

166

}

167

168

private ArrayList<Tuple<String, String>> getTemplatePlaceNames(TimedArcPetriNetNetwork network) {

169

ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();

170

for(TimedArcPetriNet tapn : network.templates()) {

171

for(TimedPlace p : tapn.places()) {

172

templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));

173

}

174

}

175

176

for(TimedPlace p : network.sharedPlaces()) {

177

templatePlaceNames.add(new Tuple<String, String>("", p.name()));

178

}

179

return templatePlaceNames;

180

}

181

182

private Arc parseAndAddTimedOutputArc(String idInput, boolean taggedArc,

183

String inscriptionTempStorage, PlaceTransitionObject sourceIn,

184

PlaceTransitionObject targetIn, double _startx, double _starty,

185

double _endx, double _endy) throws FormatException {

186

187

Arc tempArc;

188

tempArc = new TimedOutputArcComponent(_startx, _starty, _endx, _endy,

189

sourceIn, targetIn, Integer.valueOf(inscriptionTempStorage), idInput, taggedArc);

190

191

TimedPlace place = tapn.getPlaceByName(targetIn.getName());

192

TimedTransition transition = tapn.getTransitionByName(sourceIn.getName());

193

194

TimedOutputArc outputArc = new TimedOutputArc(transition, place);

195

((TimedOutputArcComponent) tempArc).setUnderlyingArc(outputArc);

196

197

if(tapn.hasArcFromTransitionToPlace(outputArc.source(),outputArc.destination())) {

198

throw new FormatException("Multiple arcs between a place and a transition is not allowed");

199

}

200

201

guiModel.addPetriNetObject(tempArc);

202

addListeners(tempArc);

203

tapn.add(outputArc);

204

205

sourceIn.addConnectFrom(tempArc);

206

targetIn.addConnectTo(tempArc);

207

return tempArc;

208

}

209

210

private Arc parseAndAddTransportArc(String idInput, boolean taggedArc,

211

String inscriptionTempStorage, PlaceTransitionObject sourceIn,

212

PlaceTransitionObject targetIn, double _startx, double _starty,

213

double _endx, double _endy) {

214

215

Arc tempArc;

216

String[] inscriptionSplit = {};

217

if (inscriptionTempStorage.contains(":")) {

218

inscriptionSplit = inscriptionTempStorage.split(":");

219

}

220

boolean isInPreSet = false;

221

if (sourceIn instanceof Place) {

222

isInPreSet = true;

223

}

224

tempArc = new TransportArcComponent(new TimedInputArcComponent(

225

new TimedOutputArcComponent(_startx, _starty, _endx, _endy, sourceIn, targetIn, 1, idInput, taggedArc),

226

inscriptionSplit[0]), Integer.parseInt(inscriptionSplit[1]), isInPreSet);

227

228

sourceIn.addConnectFrom(tempArc);

229

targetIn.addConnectTo(tempArc);

230

231

if (isInPreSet) {

232

if (postsetArcs.containsKey((TimedTransitionComponent) targetIn)) {

233

TransportArcComponent postsetTransportArc = postsetArcs.get((TimedTransitionComponent) targetIn);

234

TimedPlace sourcePlace = tapn.getPlaceByName(sourceIn.getName());

235

TimedTransition trans = tapn.getTransitionByName(targetIn.getName());

236

TimedPlace destPlace = tapn.getPlaceByName(postsetTransportArc.getTarget().getName());

237

TimeInterval interval = TimeInterval.parse(inscriptionSplit[0], constants);

238

239

assert (sourcePlace != null);

240

assert (trans != null);

241

assert (destPlace != null);

242

243

TransportArc transArc = new TransportArc(sourcePlace, trans, destPlace, interval);

244

245

((TransportArcComponent) tempArc).setUnderlyingArc(transArc);

246

postsetTransportArc.setUnderlyingArc(transArc);

247

guiModel.addPetriNetObject(tempArc);

248

addListeners(tempArc);

249

guiModel.addPetriNetObject(postsetTransportArc);

250

addListeners(postsetTransportArc);

251

tapn.add(transArc);

252

253

postsetArcs.remove((TimedTransitionComponent) targetIn);

254

} else {

255

presetArcs.put((TimedTransitionComponent) targetIn, (TransportArcComponent) tempArc);

256

transportArcsTimeIntervals.put((TransportArcComponent) tempArc, TimeInterval.parse(inscriptionSplit[0], constants));

257

}

258

} else {

259

if (presetArcs.containsKey((TimedTransitionComponent) sourceIn)) {

260

TransportArcComponent presetTransportArc = presetArcs.get((TimedTransitionComponent) sourceIn);

261

TimedPlace sourcePlace = tapn.getPlaceByName(presetTransportArc.getSource().getName());

262

TimedTransition trans = tapn.getTransitionByName(sourceIn.getName());

263

TimedPlace destPlace = tapn.getPlaceByName(targetIn.getName());

264

TimeInterval interval = transportArcsTimeIntervals.get((TransportArcComponent) presetTransportArc);

265

266

assert (sourcePlace != null);

267

assert (trans != null);

268

assert (destPlace != null);

269

270

TransportArc transArc = new TransportArc(sourcePlace, trans,

271

destPlace, interval);

272

273

((TransportArcComponent) tempArc).setUnderlyingArc(transArc);

274

presetTransportArc.setUnderlyingArc(transArc);

275

guiModel.addPetriNetObject(presetTransportArc);

276

addListeners(presetTransportArc);

277

guiModel.addPetriNetObject(tempArc);

278

addListeners(tempArc);

279

tapn.add(transArc);

280

281

presetArcs.remove((TimedTransitionComponent) sourceIn);

282

transportArcsTimeIntervals.remove((TransportArcComponent) presetTransportArc);

283

} else {

284

postsetArcs.put((TimedTransitionComponent) sourceIn, (TransportArcComponent) tempArc);

285

}

286

}

287

return tempArc;

288

}

289

290

private Arc parseAndAddTimedInputArc(String idInput, boolean taggedArc,

291

String inscriptionTempStorage, PlaceTransitionObject sourceIn,

292

PlaceTransitionObject targetIn, double _startx, double _starty,

293

double _endx, double _endy) throws FormatException {

294

Arc tempArc;

295

tempArc = new TimedInputArcComponent(new TimedOutputArcComponent(

296

_startx, _starty, _endx, _endy, sourceIn, targetIn, 1, idInput,

297

taggedArc),

298

(inscriptionTempStorage != null ? inscriptionTempStorage : ""));

299

300

TimedPlace place = tapn.getPlaceByName(sourceIn.getName());

301

TimedTransition transition = tapn.getTransitionByName(targetIn.getName());

302

TimeInterval interval = TimeInterval.parse(inscriptionTempStorage, constants);

303

304

TimedInputArc inputArc = new TimedInputArc(place, transition, interval);

305

((TimedInputArcComponent) tempArc).setUnderlyingArc(inputArc);

306

307

if(tapn.hasArcFromPlaceToTransition(inputArc.source(), inputArc.destination())) {

308

throw new FormatException("Multiple arcs between a place and a transition is not allowed");

309

}

310

311

guiModel.addPetriNetObject(tempArc);

312

addListeners(tempArc);

313

tapn.add(inputArc);

314

315

sourceIn.addConnectFrom(tempArc);

316

targetIn.addConnectTo(tempArc);

317

return tempArc;

318

}

319

320

private Arc parseAndAddTimedInhibitorArc(String idInput, boolean taggedArc,

321

String inscriptionTempStorage, PlaceTransitionObject sourceIn,

322

PlaceTransitionObject targetIn, double _startx, double _starty,

323

double _endx, double _endy) {

324

Arc tempArc;

325

tempArc = new TimedInhibitorArcComponent(

326

new TimedInputArcComponent(

327

new TimedOutputArcComponent(_startx, _starty, _endx, _endy, sourceIn, targetIn, 1, idInput, taggedArc)

328

329

(inscriptionTempStorage != null ? inscriptionTempStorage : ""));

330

TimedPlace place = tapn.getPlaceByName(sourceIn.getName());

331

TimedTransition transition = tapn.getTransitionByName(targetIn.getName());

332

TimeInterval interval = TimeInterval.parse(inscriptionTempStorage, constants);

333

334

if(!interval.equals(TimeInterval.ZERO_INF) && firstInhibitorIntervalWarning) {

335

JOptionPane.showMessageDialog(CreateGui.getApp(), "The chosen model contained inhibitor arcs with unsupported intervals.\n\nTAPAAL only supports inhibitor arcs with intervals [0,inf).\n\nAny other interval on inhibitor arcs will be replaced with [0,inf).", "Unsupported Interval Detected on Inhibitor Arc", JOptionPane.INFORMATION_MESSAGE);

336

firstInhibitorIntervalWarning = false;

337

}

338

339

TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, interval);

340

341

((TimedInhibitorArcComponent) tempArc).setUnderlyingArc(inhibArc);

342

guiModel.addPetriNetObject(tempArc);

343

addListeners(tempArc);

344

tapn.add(inhibArc);

345

346

sourceIn.addConnectFrom(tempArc);

347

targetIn.addConnectTo(tempArc);

348

return tempArc;

349

}

350

351

private ReductionOption getQueryReductionOption(Element queryElement) {

352

ReductionOption reductionOption;

353

try {

354

reductionOption = ReductionOption.valueOf(queryElement.getAttribute("reductionOption"));

355

} catch (Exception e) {

356

reductionOption = ReductionOption.STANDARD;

357

}

358

return reductionOption;

359

}

360

361

private ExtrapolationOption getQueryExtrapolationOption(Element queryElement) {

362

ExtrapolationOption extrapolationOption;

363

try {

364

extrapolationOption = ExtrapolationOption.valueOf(queryElement.getAttribute("extrapolationOption"));

365

} catch (Exception e) {

366

extrapolationOption = ExtrapolationOption.AUTOMATIC;

367

}

368

return extrapolationOption;

369

}

370

371

private HashTableSize getQueryHashTableSize(Element queryElement) {

372

HashTableSize hashTableSize;

373

try {

374

hashTableSize = HashTableSize.valueOf(queryElement.getAttribute("hashTableSize"));

375

} catch (Exception e) {

376

hashTableSize = HashTableSize.MB_16;

377

}

378

return hashTableSize;

379

}

380

381

private SearchOption getQuerySearchOption(Element queryElement) {

382

SearchOption searchOption;

383

try {

384

searchOption = SearchOption.valueOf(queryElement.getAttribute("searchOption"));

385

} catch (Exception e) {

386

searchOption = SearchOption.BFS;

387

}

388

return searchOption;

389

}

390

391

private TraceOption getQueryTraceOption(Element queryElement) {

392

TraceOption traceOption;

393

try {

394

traceOption = TraceOption.valueOf(queryElement.getAttribute("traceOption"));

395

} catch (Exception e) {

396

traceOption = TraceOption.NONE;

397

}

398

return traceOption;

399

}

400

401

private String getQueryComment(Element queryElement) {

402

String comment;

403

try {

404

comment = queryElement.getAttribute("name");

405

} catch (Exception e) {

406

comment = "No comment specified";

407

}

408

return comment;

409

}

410

411

private void parseAndAddConstant(Element constantElement) {

412

String name = constantElement.getAttribute("name");

413

int value = Integer.parseInt(constantElement.getAttribute("value"));

414

415

if (!name.isEmpty() && !name.equals(""))

416

constants.put(name, new Constant(name, value));

417

}

418

419

// //////////////////////////////////////////////////////////

420

// Legacy support for old format

421

// //////////////////////////////////////////////////////////

422

private Template parseTimedArcPetriNetAsOldFormat(Node tapnNode, TimedArcPetriNetNetwork network) throws FormatException {

423

tapn = new TimedArcPetriNet(nameGenerator .getNewTemplateName());

424

network.add(tapn);

425

426

guiModel = new DataLayer();

427

428

Node node = null;

429

NodeList nodeList = null;

430

431

nodeList = tapnNode.getChildNodes();

432

for (int i = 0; i < nodeList.getLength(); i++) {

433

node = nodeList.item(i);

434

parseElementAsOldFormat(node, tapn.name(), network.marking());

435

}

436

437

return new Template(tapn, guiModel);

438

}

439

440

private void parseElementAsOldFormat(Node node, String templateName, TimedMarking marking) throws FormatException {

441

Element element;

442

if (node instanceof Element) {

443

element = (Element) node;

444

if ("labels".equals(element.getNodeName())) {

445

parseAndAddAnnotationAsOldFormat(element);

446

} else if ("place".equals(element.getNodeName())) {

447

parseAndAddPlaceAsOldFormat(element, marking);

448

} else if ("transition".equals(element.getNodeName())) {

449

parseAndAddTransitionAsOldFormat(element);

450

} else if ("arc".equals(element.getNodeName())) {

451

parseAndAddArcAsOldFormat(element);

452

} else if ("queries".equals(element.getNodeName())) {

453

TAPNQuery query = parseQueryAsOldFormat(element);

454

455

456

if (query != null) {

457

query.getProperty().accept(new AddTemplateVisitor(templateName), null);

458

queries.add(query);

459

}

460

}

461

}

462

}

463

464

private boolean doesPlacesUsedInQueryExist(TAPNQuery query, ArrayList<Tuple<String, String>> templatePlaceNames) {

465

VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames);

466

467

VerifyPlaceNamesVisitor.Context c = nameChecker.VerifyPlaceNames(query.getProperty());

468

469

return c.getResult();

470

}

471

472

private void parseAndAddAnnotationAsOldFormat(Element inputLabelElement) throws FormatException {

473

int positionXInput = 0;

474

int positionYInput = 0;

475

int widthInput = 0;

476

int heightInput = 0;

477

boolean borderInput = true;

478

479

String positionXTempStorage = inputLabelElement.getAttribute("x");

480

String positionYTempStorage = inputLabelElement.getAttribute("y");

481

String widthTemp = inputLabelElement.getAttribute("width");

482

String heightTemp = inputLabelElement.getAttribute("height");

483

String borderTemp = inputLabelElement.getAttribute("border");

484

485

String text = getFirstChildNodeByName(inputLabelElement, "text").getTextContent();

486

487

if (positionXTempStorage.length() > 0) {

488

positionXInput = Integer.valueOf(positionXTempStorage).intValue() + 1;

489

}

490

491

if (positionYTempStorage.length() > 0) {

492

positionYInput = Integer.valueOf(positionYTempStorage).intValue() + 1;

493

}

494

495

if (widthTemp.length() > 0) {

496

widthInput = Integer.valueOf(widthTemp).intValue() + 1;

497

}

498

499

if (heightTemp.length() > 0) {

500

heightInput = Integer.valueOf(heightTemp).intValue() + 1;

501

}

502

503

if (borderTemp.length() > 0) {

504

borderInput = Boolean.valueOf(borderTemp).booleanValue();

505

} else {

506

borderInput = true;

507

}

508

AnnotationNote an = new AnnotationNote(text, positionXInput,

509

positionYInput, widthInput, heightInput, borderInput);

510

guiModel.addPetriNetObject(an);

511

addListeners(an);

512

}

513

514

private void parseAndAddTransitionAsOldFormat(Element element) throws FormatException {

515

double positionXInput = getPositionAttribute(element, "x");

516

double positionYInput = getPositionAttribute(element, "y");

517

String idInput = element.getAttribute("id");

518

String nameInput = getChildNodesContentOfValueChildNodeAsString(element, "name");

519

double nameOffsetXInput = getNameOffsetAttribute(element, "x");

520

double nameOffsetYInput = getNameOffsetAttribute(element, "y");

521

boolean timedTransition = getContentOfFirstSpecificChildNodesValueChildNodeAsBoolean(element, "timed");

522

boolean infiniteServer = getContentOfFirstSpecificChildNodesValueChildNodeAsBoolean(element, "infiniteServer");

523

int angle = getContentOfFirstSpecificChildNodesValueChildNodeAsInt(element,"orientation");

524

int priority = getContentOfFirstSpecificChildNodesValueChildNodeAsInt(element,"priority");

525

526

positionXInput = Grid.getModifiedX(positionXInput);

527

positionYInput = Grid.getModifiedY(positionYInput);

528

529

if (idInput.length() == 0 && nameInput.length() > 0) {

530

idInput = nameInput;

531

}

532

533

if (nameInput.length() == 0 && idInput.length() > 0) {

534

nameInput = idInput;

535

}

536

537

TimedTransition t = new TimedTransition(nameInput);

538

539

TimedTransitionComponent transition = new TimedTransitionComponent(

540

positionXInput, positionYInput, idInput, nameInput,

541

nameOffsetXInput, nameOffsetYInput, timedTransition,

542

infiniteServer, angle, priority);

543

transition.setUnderlyingTransition(t);

544

transition.setTimed(true);

545

guiModel.addPetriNetObject(transition);

546

addListeners(transition);

547

tapn.add(t);

548

}

549

550

private void parseAndAddPlaceAsOldFormat(Element element, TimedMarking marking) throws FormatException {

551

double positionXInput = getPositionAttribute(element, "x");

552

double positionYInput = getPositionAttribute(element, "y");

553

String idInput = element.getAttribute("id");

554

String nameInput = getChildNodesContentOfValueChildNodeAsString(element, "name");

555

double nameOffsetXInput = getNameOffsetAttribute(element, "x");

556

double nameOffsetYInput = getNameOffsetAttribute(element, "y");

557

int initialMarkingInput = getContentOfFirstSpecificChildNodesValueChildNodeAsInt(element, "initialMarking");

558

double markingOffsetXInput = getMarkingOffsetAttribute(element, "x");

559

double markingOffsetYInput = getMarkingOffsetAttribute(element, "y");

560

int capacityInput = getContentOfFirstSpecificChildNodesValueChildNodeAsInt(element, "capacity");

561

String invariant = getChildNodesContentOfValueChildNodeAsString(element, "invariant");

562

563

positionXInput = Grid.getModifiedX(positionXInput);

564

positionYInput = Grid.getModifiedY(positionYInput);

565

566

if (idInput.length() == 0 && nameInput.length() > 0) {

567

idInput = nameInput;

568

}

569

570

if (nameInput.length() == 0 && idInput.length() > 0) {

571

nameInput = idInput;

572

}

573

574

Place place = null;

575

576

if (invariant == null || invariant == "") {

577

place = new Place(positionXInput, positionYInput, idInput,

578

nameInput, nameOffsetXInput, nameOffsetYInput,

579

initialMarkingInput, markingOffsetXInput,

580

markingOffsetYInput, capacityInput);

581

582

} else {

583

place = new TimedPlaceComponent(positionXInput, positionYInput,

584

idInput, nameInput, nameOffsetXInput, nameOffsetYInput,

585

initialMarkingInput, markingOffsetXInput,

586

markingOffsetYInput, capacityInput);

587

588

LocalTimedPlace p = new LocalTimedPlace(nameInput, TimeInvariant.parse(invariant, constants));

589

tapn.add(p);

590

591

((TimedPlaceComponent) place).setUnderlyingPlace(p);

592

guiModel.addPetriNetObject(place);

593

addListeners(place);

594

595

for (int i = 0; i < initialMarkingInput; i++) {

596

marking.add(new TimedToken(p, new BigDecimal(0.0)));

597

}

598

}

599

}

600

601

private void parseAndAddArcAsOldFormat(Element inputArcElement) throws FormatException {

602

String idInput = inputArcElement.getAttribute("id");

603

String sourceInput = inputArcElement.getAttribute("source");

604

String targetInput = inputArcElement.getAttribute("target");

605

boolean taggedArc = getContentOfFirstSpecificChildNodesValueChildNodeAsBoolean(inputArcElement, "tagged");

606

String inscriptionTempStorage = getChildNodesContentOfValueChildNodeAsString(inputArcElement, "inscription");

607

608

PlaceTransitionObject sourceIn = guiModel.getPlaceTransitionObject(sourceInput);

609

PlaceTransitionObject targetIn = guiModel.getPlaceTransitionObject(targetInput);

610

611

// add the insets and offset

612

int aStartx = sourceIn.getX() + sourceIn.centreOffsetLeft();

613

int aStarty = sourceIn.getY() + sourceIn.centreOffsetTop();

614

615

int aEndx = targetIn.getX() + targetIn.centreOffsetLeft();

616

int aEndy = targetIn.getY() + targetIn.centreOffsetTop();

617

618

double _startx = aStartx;

619

double _starty = aStarty;

620

double _endx = aEndx;

621

double _endy = aEndy;

622

623

Arc tempArc;

624

625

String type = "normal";

626

type = ((Element) getFirstChildNodeByName(inputArcElement, "type")).getAttribute("value");

627

628

if (type.equals("tapnInhibitor")) {

629

630

tempArc = parseAndAddTimedInhibitorArc(idInput, taggedArc,

631

inscriptionTempStorage, sourceIn, targetIn, _startx,

632

_starty, _endx, _endy);

633

634

} else {

635

if (type.equals("timed")) {

636

tempArc = parseAndAddTimedInputArc(idInput, taggedArc,

637

inscriptionTempStorage, sourceIn, targetIn, _startx,

638

_starty, _endx, _endy);

639

640

} else if (type.equals("transport")) {

641

tempArc = parseAndAddTransportArc(idInput, taggedArc,

642

inscriptionTempStorage, sourceIn, targetIn, _startx,

643

_starty, _endx, _endy);

644

645

} else {

646

tempArc = parseAndAddTimedOutputArc(idInput, taggedArc,

647

inscriptionTempStorage, sourceIn, targetIn, _startx,

648

_starty, _endx, _endy);

649

}

650

651

}

652

653

parseArcPathAsOldFormat(inputArcElement, tempArc);

654

}

655

656

private void parseArcPathAsOldFormat(Element inputArcElement, Arc tempArc) {

657

NodeList nodelist = inputArcElement.getElementsByTagName("arcpath");

658

if (nodelist.getLength() > 0) {

659

tempArc.getArcPath().purgePathPoints();

660

for (int i = 0; i < nodelist.getLength(); i++) {

661

Node node = nodelist.item(i);

662

if (node instanceof Element) {

663

Element element = (Element) node;

664

if ("arcpath".equals(element.getNodeName())) {

665

String arcTempX = element.getAttribute("x");

666

String arcTempY = element.getAttribute("y");

667

String arcTempType = element.getAttribute("curvePoint");

668

float arcPointX = Float.valueOf(arcTempX).floatValue();

669

float arcPointY = Float.valueOf(arcTempY).floatValue();

670

arcPointX += Pipe.ARC_CONTROL_POINT_CONSTANT + 1;

671

arcPointY += Pipe.ARC_CONTROL_POINT_CONSTANT + 1;

672

boolean arcPointType = Boolean.valueOf(arcTempType).booleanValue();

673

tempArc.getArcPath().addPoint(arcPointX, arcPointY, arcPointType);

674

}

675

}

676

}

677

}

678

}

679

680

private TAPNQuery parseQueryAsOldFormat(Element queryElement) throws FormatException {

681

String comment = getQueryComment(queryElement);

682

TraceOption traceOption = getQueryTraceOption(queryElement);

683

SearchOption searchOption = getQuerySearchOption(queryElement);

684

HashTableSize hashTableSize = getQueryHashTableSize(queryElement);

685

ExtrapolationOption extrapolationOption = getQueryExtrapolationOption(queryElement);

686

ReductionOption reductionOption = getQueryReductionOption(queryElement);

687

int capacity = getQueryCapacityAsOldFormat(queryElement);

688

689

TCTLAbstractProperty query;

690

query = parseQueryPropertyAsOldFormat(queryElement);

691

692

if (query != null)

693

return new TAPNQuery(comment, capacity, query, traceOption,

694

searchOption, reductionOption, hashTableSize,

695

extrapolationOption);

696

else

697

return null;

698

}

699

700

private TCTLAbstractProperty parseQueryPropertyAsOldFormat(Element queryElement) throws FormatException {

701

TCTLAbstractProperty query = null;

702

TAPAALQueryParser queryParser = new TAPAALQueryParser();

703

704

String queryToParse = getChildNodesContentOfValueChildNodeAsString(queryElement, "query");

705

706

try {

707

query = queryParser.parse(queryToParse);

708

} catch (Exception e) {

709

if(firstQueryParsingWarning ) {

710

JOptionPane.showMessageDialog(CreateGui.getApp(), ERROR_PARSING_QUERY_MESSAGE, "Error Parsing Query", JOptionPane.ERROR_MESSAGE);

711

firstQueryParsingWarning = false;

712

}

713

System.err.println("No query was specified: " + e.getStackTrace());

714

}

715

return query;

716

}

717

718

private int getQueryCapacityAsOldFormat(Element queryElement) throws FormatException {

719

return getContentOfFirstSpecificChildNodesValueChildNodeAsInt(queryElement, "capacity");

720

}

721

722

private boolean getContentOfFirstSpecificChildNodesValueChildNodeAsBoolean(Element element, String childNodeName) throws FormatException {

723

Node node = getFirstChildNodeByName(element, childNodeName);

724

725

if (node instanceof Element) {

726

Element e = (Element) node;

727

728

String value = getContentOfValueChildNode(e);

729

730

return Boolean.parseBoolean(value);

731

}

732

733

return false;

734

}

735

736

private double getNameOffsetAttribute(Element element, String coordinateName) throws FormatException {

737

Node node = getFirstChildNodeByName(element, "name");

738

739

if (node instanceof Element) {

740

Element e = (Element) node;

741

742

Element graphics = ((Element) getFirstChildNodeByName(e, "graphics"));

743

String offsetCoordinate = ((Element) getFirstChildNodeByName(graphics, "offset")).getAttribute(coordinateName);

744

if (offsetCoordinate.length() > 0) {

745

return Double.valueOf(offsetCoordinate).doubleValue();

746

}

747

}

748

749

return 0.0;

750

}

751

752

private Node getFirstChildNodeByName(Element element, String childNodeName) throws FormatException {

753

Node node = element.getElementsByTagName(childNodeName).item(0);

754

755

if (node == null)

756

throw new FormatException("TAPAAL could not recognize save format.");

757

758

return node;

759

}

760

761

private String getContentOfValueChildNode(Element element) throws FormatException {

762

return ((Element) getFirstChildNodeByName(element, "value")).getTextContent();

763

}

764

765

private String getChildNodesContentOfValueChildNodeAsString(Element element, String childNodeName) throws FormatException {

766

Node node = getFirstChildNodeByName(element, childNodeName);

767

768

if (node instanceof Element) {

769

Element e = (Element) node;

770

771

return getContentOfValueChildNode(e);

772

}

773

774

return "";

775

}

776

777

private double getPositionAttribute(Element element, String coordinateName) throws FormatException {

778

Node node = getFirstChildNodeByName(element, "graphics");

779

780

if (node instanceof Element) {

781

Element e = (Element) node;

782

783

String posCoordinate = ((Element) getFirstChildNodeByName(e, "position")).getAttribute(coordinateName);

784

if (posCoordinate.length() > 0) {

785

return Double.valueOf(posCoordinate).doubleValue();

786

}

787

}

788

789

return 0.0;

790

}

791

792

private int getContentOfFirstSpecificChildNodesValueChildNodeAsInt(Element element, String childNodeName) throws FormatException {

793

Node node = getFirstChildNodeByName(element, childNodeName);

794

795

if (node instanceof Element) {

796

Element e = (Element) node;

797

798

String value = getContentOfValueChildNode(e);

799

800

if (value.length() > 0)

801

return Integer.parseInt(value);

802

}

803

804

return 0;

805

}

806

807

private double getMarkingOffsetAttribute(Element element, String coordinateName) throws FormatException {

808

Node node = getFirstChildNodeByName(element, "initialMarking");

809

810

if (node instanceof Element) {

811

Element e = (Element) node;

812

813

Element graphics = ((Element) getFirstChildNodeByName(e, "graphics"));

814

String offsetCoordinate = ((Element) getFirstChildNodeByName(graphics, "offset")).getAttribute(coordinateName);

815

if (offsetCoordinate.length() > 0)

816

return Double.parseDouble(offsetCoordinate);

817

}

818

819

return 0.0;

820

}

821

822

private void addListeners(PetriNetObject newObject) {

823

if (newObject != null) {

824

if (newObject.getMouseListeners().length == 0) {

825

if (newObject instanceof Place) {

826

// XXX - kyrke

827

if (newObject instanceof TimedPlaceComponent) {

828

829

LabelHandler labelHandler = new LabelHandler(((Place) newObject).getNameLabel(), (Place) newObject);

830

((Place) newObject).getNameLabel().addMouseListener(labelHandler);

831

((Place) newObject).getNameLabel().addMouseMotionListener(labelHandler);

832

((Place) newObject).getNameLabel().addMouseWheelListener(labelHandler);

833

834

PlaceHandler placeHandler = new PlaceHandler(drawingSurface, (Place) newObject, guiModel, tapn);

835

newObject.addMouseListener(placeHandler);

836

newObject.addMouseWheelListener(placeHandler);

837

newObject.addMouseMotionListener(placeHandler);

838

} else {

839

840

LabelHandler labelHandler = new LabelHandler(((Place) newObject).getNameLabel(), (Place) newObject);

841

((Place) newObject).getNameLabel().addMouseListener(labelHandler);

842

((Place) newObject).getNameLabel().addMouseMotionListener(labelHandler);

843

((Place) newObject).getNameLabel().addMouseWheelListener(labelHandler);

844

845

PlaceHandler placeHandler = new PlaceHandler(drawingSurface, (Place) newObject);

846

newObject.addMouseListener(placeHandler);

847

newObject.addMouseWheelListener(placeHandler);

848

newObject.addMouseMotionListener(placeHandler);

849

850

}

851

} else if (newObject instanceof Transition) {

852

TransitionHandler transitionHandler;

853

if (newObject instanceof TimedTransitionComponent) {

854

transitionHandler = new TAPNTransitionHandler(drawingSurface, (Transition) newObject, guiModel, tapn);

855

} else {

856

transitionHandler = new TransitionHandler(drawingSurface, (Transition) newObject);

857

}

858

859

LabelHandler labelHandler = new LabelHandler(((Transition) newObject).getNameLabel(), (Transition) newObject);

860

((Transition) newObject).getNameLabel().addMouseListener(labelHandler);

861

((Transition) newObject).getNameLabel().addMouseMotionListener(labelHandler);

862

((Transition) newObject).getNameLabel().addMouseWheelListener(labelHandler);

863

864

newObject.addMouseListener(transitionHandler);

865

newObject.addMouseMotionListener(transitionHandler);

866

newObject.addMouseWheelListener(transitionHandler);

867

868

newObject.addMouseListener(new AnimationHandler());

869

870

} else if (newObject instanceof Arc) {

871

/* CB - Joakim Byg add timed arcs */

872

if (newObject instanceof TimedInputArcComponent) {

873

if (newObject instanceof TransportArcComponent) {

874

TransportArcHandler transportArcHandler = new TransportArcHandler(drawingSurface, (Arc) newObject);

875

newObject.addMouseListener(transportArcHandler);

876

newObject.addMouseWheelListener(transportArcHandler);

877

newObject.addMouseMotionListener(transportArcHandler);

878

} else {

879

TimedArcHandler timedArcHandler = new TimedArcHandler(drawingSurface, (Arc) newObject);

880

newObject.addMouseListener(timedArcHandler);

881

newObject.addMouseWheelListener(timedArcHandler);

882

newObject.addMouseMotionListener(timedArcHandler);

883

}

884

} else {

885

/* EOC */

886

ArcHandler arcHandler = new ArcHandler(drawingSurface,(Arc) newObject);

887

newObject.addMouseListener(arcHandler);

888

newObject.addMouseWheelListener(arcHandler);

889

newObject.addMouseMotionListener(arcHandler);

890

}

891

} else if (newObject instanceof AnnotationNote) {

892

AnnotationNoteHandler noteHandler = new AnnotationNoteHandler(drawingSurface, (AnnotationNote) newObject);

893

newObject.addMouseListener(noteHandler);

894

newObject.addMouseMotionListener(noteHandler);

895

((Note) newObject).getNote().addMouseListener(noteHandler);

896

((Note) newObject).getNote().addMouseMotionListener(noteHandler);

897

}

898

if (newObject instanceof Zoomable) {

899

newObject.zoomUpdate(drawingSurface.getZoom());

900

}

901

}

902

newObject.setGuiModel(guiModel);

903

}

904

}

905

}

Older »