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

## 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 ${\displaystyle \square (q\wedge \circ q)}$, so it does not satisfy ${\displaystyle \neg \square (q\wedge \circ q)}$ 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 ${\displaystyle \square (q\vee \circ q)}$ 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 ${\displaystyle \neg \square (q\vee \circ q)}$, not ${\displaystyle \square (q\vee \circ q)}$. Therefore is enough to show that 1 computation does not fulfill ${\displaystyle \neg \square (q\vee \circ q)}$, i.e., that it fulfills ${\displaystyle \square (q\vee \circ q)}$. 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 ${\displaystyle t\in P(AP)^{\omega }}$. 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)