** Master project?
The Uppaal model checker does not support many of the features in SMC (the double type, mixing clock and data variables in certain expressions etc.).
This leaves SMC in a semi-supported state by UrPal.
To solve this, we need to transform SMC models by removing the unsupported SMC features, while keeping changes to the model behavior to a minimum. Most importantly, reachability properties should be unchanged.
** Master project? The Uppaal model checker does not support many of the features in SMC (the double type, mixing clock and data variables in certain expressions etc.).
This leaves SMC in a semi-supported state by UrPal.
To solve this, we need to transform SMC models by removing the unsupported SMC features, while keeping changes to the model behavior to a minimum. Most importantly, reachability properties should be unchanged.