Bug 544

Summary: support for clock and random initialisers (initializers)
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: enhancement    
Priority: P5    
Version: 4.1.13   
Hardware: All   
OS: All   
Architecture:
Attachments: non-zero initializer break invariant in initial location

Description Marius Mikučionis 2013-01-17 11:22:48 CET
There are two problems:

1) default clock initialiser (0) obscures SMC models by having value zero which does not always make sense, it also obscures query results (see bug 543)

2) stochastic and dynamical systems may have random initial states, it would be convenient to define it with initialiser.
Comment 1 Marius Mikučionis 2017-04-06 13:41:05 CEST
Created attachment 309 [details]
non-zero initializer break invariant in initial location