PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

Add the syntax checking after parsing to rule out invalid/un-declared variables usage

The parser is completely re-designed. Now the AST is built up and parsed using two time parsing process.

The two time parsing make it much easier to detect the un-declared variables and duplicated definitions.

The improvements are:
1 Constants can be declared at any place of the specification.
2 Un-declared variables and channel names are not allowed. Record variables are different from normal variables.
3 Same name is not allowed for different constants, global variables, channels names, LTL propersition names, and process names.
4 Constants, global variables, channels names, LTL propersition names, and process names are not allowed to be used as events names.