search

Ecdar / j-Ecdar

A model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems) written in Java.
MIT License
4 stars 9 forks source link

Automaton constructor Clocks and Boolean variables #67

Open Brandhoej opened 2 years ago

Brandhoej commented 2 years ago

The Automaton constructor takes a list of Clock and one with BoolVar. We should consider checking whether all clocks and boolean variables are present in the guards and update.

magoorden commented 2 years ago

I think this is a good check to perform, but violating this check does not invalidate a model, i.e., an automaton that has a clock which is never 'used' is still a valid model. So this should be something like a warning instead of an error.