Non-increasing monotonic tag relations forbidden ?

heron-solver / heron

🏺 Simulation Solver for Timed Causality Models in TESL

MIT License

5 stars 1 forks source link

Non-increasing monotonic tag relations forbidden ? #27

Closed hai-nguyen-van closed 6 years ago

hai-nguyen-van commented 7 years ago

rational-clock c1 sporadic 1.0, 2.0, 3.0
rational-clock c2 sporadic -1.0

tag relation c1 = -1.0 * c2

Infinitely derivable. Raises the question: does an infinitely-derivable configuration a satisfying one?

hai-nguyen-van commented 6 years ago

Time is allowed to stutter. Yet, the specification is unsolvable. Hence, an infinitely-derivable specification is not necessarily satisfying. It appears to be, under conditions that consuming sporadic doesn't fall into deadlock as it is above...