imitator-model-checker / imitator

IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.

https://www.imitator.fr/

GNU General Public License v3.0

26 stars 12 forks source link

Add some non regression tests on user functions #122

Open lbinria opened 2 years ago

lbinria commented 2 years ago

Description

Make non regression tests on user functions:

General tests, testing the behavior of different user functions with different types
Check that an error is raised when using a user function that is subjet to side effects in guard / invariant continuous update, property
Check that an error is raised when trying to update a clock or parameter
Check that an error is raised when duplicate parameters
Check we can use user function in properties