Muc Thaonp

Readme document

Component Bean

Assembly Test


-In this file, I declare the node TicketChecker(bool) with the following functionality:

  • When a customer arrives, the node returns the number of customer already already in the cinema (including the new one have just arrived). In another words, the TicketChecker counts the number of customer in the cinema and emit the new value whenever a customer arrives.
  • The counting function is implemented by node Increase(Number: int)

- I also declare the node TickerChecker_verif(bool) to verify the correctness of node TickerChecker with the above specification.

  • The property to be proved is that the outcome of the node TickerChecker must be different from its previous value if a customer arrives and be the same if no customer arrives.

TicketChecker.c & TicketChecker.h

- These are corresponding C code generated from the TickerChecker.lus file.


- This is an executive file compiled from generated C code.
- The C code is generated using the command: ec2c -loop


- This is the native dll file that I created from C code files: TicketChecker.c and TicketChecker.h
- I used SharpDevelop to create this dll file.
- It is put in folder Lib.


- This is the bean component that I created from ConsoleApp.dll
- The source code to create this bean is Bean1.cs


- This container is an assembly to test the bean component TicketChecker.dll

Unclear, need to ask the teachers, since most is obviously derived works.