Description of Flashing Light

[nasa-sw-vnv]

Description of Flashing Light

[tpressburger]

Thank you for your interesting scenario! I think you have formulated correctly in your first requirement entering and leaving toggling mode. I think you understand the semantics of unless. However, as there should always be two lamps off, that means that two of the last three of your requirements will be applicable, hence specifying that more than one lamp be on at the same time. Also, saying "after 1 second !L3" doesn't preclude L3 turning back on after two seconds, nor does it preclude L2 or L1 also being on at the same time for 1 second.

So I think a solution is the following (I simplified the example to not specify toggling mode):

1. The sys shall immediately satisfy L1 & !L2 & !L3
2. Upon L1 the sys shall for 1 sec satisfy L1 & !L2 & !L3
3. Upon L2 the sys shall for 1 sec satisfy L2 & !L1 & !L3
4. Upon L3 the sys shall for 1 sec satisfy L3 & !L1 & !L2
5. Upon L1 the sys shall after 1 sec satisfy L2
6. Upon L2 the sys shall after 1 sec satisfy L3
7. Upon L3 the sys shall after 1 sec satisfy L1

I like using the word "upon" because it implies being triggered by the proposition becoming true from false.

[leesoons]

thanks a lot!

[anmavrid]

I am closing this issue since the question has been answered.