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

Absence of check of variable existence in updates #169

Open etienneandre opened 7 months ago

etienneandre commented 7 months ago

Bug occurring in develop/486ad42 (Build date: 2024-03-06 17:45:32 UTC)

var

(************************************************************)
  automaton pta_1
(************************************************************)
actions: notify;

loc l0: invariant True
    when True sync notify do {doesntexist := 0} goto l0;

end (* pta *)

(************************************************************)
(* Initial state *)
(************************************************************)

init := {

    discrete =
        (*------------------------------------------------------------*)
        (* Initial location *)
        (*------------------------------------------------------------*)
        loc[pta_1] := l0,

        (*------------------------------------------------------------*)
        (* Initial discrete variables assignments *)
        (*------------------------------------------------------------*)

    ;

    continuous =        
        (*------------------------------------------------------------*)
        (* Initial clock constraints *)
        (*------------------------------------------------------------*)

        (*------------------------------------------------------------*)
        (* Parameter constraints *)
        (*------------------------------------------------------------*)
    ;
}

(************************************************************)
(* The end *)
(************************************************************)
end

Problem: doesntexist does not exist; and it's not detected at all!