Rule-Based Denotational Semantics 

  Assignment Goal

The goal of this assignment is to build a rule-based transformation for the denotational semantics of RPGame in the form of a mapping to your own Petri nets formalism. This is a rather large assignment, so you can complete this assignment in groups of two students. The following tasks need to be completed:
  1. Implement a rule-based transformation that transforms RPGame models into Petri net models (use PNModels from the central formalisms).
    • Make sure this transformation is complete, i.e., every well-formed RPGame model produces a well-formed Petri net.
    • Do not remove your RPGame model during transformation. Instead, keep it and create traceability links between created Places and Transitions and the RPGame element they correspond to. Use the GenericLinks formalism for traceability links. These links will greatly help in implementing your transformation.
  2. (Optional) Create an extension of your Petri net simulator, so that during simulation, the related RPGame model is updated as well. The behaviour in your RPGame model must be the same as your Python-based operational semantics and your rule-based operational semantics.
  3. Write an exporter that exports your Petri net models to pipe2 models (in PNML), so that you can re-use the tool's analysis algorithms.
    • Create a realistic example of a RPGame. Additionally, think of at least three invariants for this model. The goal is to check these invariants on your model. You will do this by transforming your model to a Petri net, export this to PNML, open this model in pipe2 and do your checks using that tool.
  4. On top of this example, create test models that test all requirements of this assignment. Make sure that your test cases maximise your confidence in the correctness of the implementation of these requirements, so keep your test coverage in mind. Your test suite should include:
    • test cases that test your RPGame to Petri net transformation;
    • test cases that test your PNML exporter.
  5. Write a report that:
    • explains the particularities of your solution and the difficulties you encountered;
    • sums up the desirable results for all your test cases (in the form of text/image).
The deadline for this assigment is December 7, 2012. You will have to submit your solution (AToM^3 files and report) to Blackboard.

  Useful Links