Diskussion:Lösungsvorschlag Formal Methods And Functional Programming FS16: Unterschied zwischen den Versionen

Aus VISki
Wechseln zu: Navigation, Suche
(Assignment 8: Comment about changes to (c).)
(Änderung 17228 von Sommemic (Diskussion) rückgängig gemacht.)
 
(Eine dazwischenliegende Version desselben Benutzers wird nicht angezeigt)
(kein Unterschied)

Aktuelle Version vom 15. August 2019, 15:48 Uhr

Assignment 6

(b)

I've changed {x=0} x:=1 {x=1} to {x+1=0} x:=x+1 {x=0}, since the first triple cannot be justified by a derivation tree, since (x=1)[x |-> 1] = (1=0), and not x=0

--Thedot (Diskussion) 11:34, 19. Jun. 2017 (CEST)

Thanks very much.

--Nacknime (Diskussion) 16:08, 19. Jun. 2017 (CEST)

Assignment 8

(a)

The solution to 3. went back and forth between valid and invalid a few times now, so maybe we could move the discussion here: According to this years slides (Model Checking, page 7) "An LTL formula is valid in a transition system, if every trace of the transition system satisfies the formula". Here this is not the case, as the computation s1, s2, s1, s2, ... satisfies , so it does not satisfy and therefore the formula is not valid.

--Aecturus (Diskussion) 10:34, 28. Jul. 2017 (CEST)

I think the recent change made by Simhuber (This comment is wrong! Since makes an claim over ALL execution paths is enough to show that 1 path is wrong and therefore this does not hold!) is wrong:

The given formula is , not . Therefore is enough to show that 1 computation does not fulfill , i.e., that it fulfills . This computation clearly exists, therefore the formula is not valid.

--Aecturus (Diskussion) 11:42, 17. Aug. 2017 (CEST)

(c)

Thedot, you say it is also a safety property, trivially because there are no traces that don't belong to P. According to the definition though, to see whether a property is safety/liveness, you not only have to consider the traces allowed by the concrete state machine, but all traces . So I think your change was wrong.

--Nacknime (Diskussion) 16:10, 19. Jun. 2017 (CEST)

Yep, my bad. Thanks for pointing my mistake out! I removed it now.

--Thedot (Diskussion) 17:16, 19. Jun. 2017 (CEST)

There was a recent change by Florianalexandermoser saying that it is a safety property. I think this is wrong and the previous answer was indeed correct. I therefore changed it back and added a link to this discussion for the future.

--Aecturus (Diskussion) 12:00, 17. Aug. 2017 (CEST)