Rule-Based Denotational Semantics 

  Assignment Goal

The goal of this assignment is to build a rule-based transformation for the denotational semantics of production systems for assembling armoured personnel carriers (APCs) 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. You can choose which of your two available Production System formalisms you will use for this assignment. The following tasks need to be completed:
  1. Implement your own Petri net formalism. Implement Tokens as a explicit entity (i.e., use a metaclass, not a meta-attribute). (Remember: in order to avoid name clashes, use in your metamodel prefixes in class names, such as "MyPN_".)
  2. Implement a rule-based Petri net simulator, i.e., the operational semantics of Petri nets. (See previous assignment.) Executing the simulator will continuously fire transitions (if enabled). Keep fairness in mind.
  3. Implement a rule-based transformation that transforms Production Systems models into Petri net models.
    • Make sure this transformation is complete, i.e., every well-formed Production System produces a well-formed Petri net.
    • Do not remove your Production Systems model during transformation. Instead, keep it and create traceability links between created Places and Transitions and the Production Systems element they correspond to. Use the GenericLinks formalism for traceability links. These links will greatly help in implementing your transformation.
  4. Create a variation of your Petri net simulator, so that during simulation, the related Production Systems model is updated as well. The behaviour in your Production System must be the same as your Python-based operational semantics and your rule-based operational semantics.
  5. 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 Production System. 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.
  6. On top of this example, write a test suite that tests all requirements of this assignment. Make sure that your test cases that 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 Petri net simulator (req. #2);
    • test cases that test your Production Systems to Petri net transformation (req. #3);
    • test cases that test your Production Systems simulator that uses your Petri net simulator (req. #4);
    • test cases that test your PNML exporter (req. #5).
  7. 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 9, 2011. You will have to submit your solution (AToM^3 files and report) to Blackboard.

  Useful Links