Spinroot

marc15

Member

Registered: 2019-02-07

Posts: 34

p U false

regarding p U false

in The SPIN model checker: Primer and reference manual is written:
"Note that the truth of this formula only depends on the value of sub-formula p."

I thought the difference between strong until and weak until is
p U q, q must become true
p W q, q can become true

so, was really p U false intended and not p W false in the meaning of always/[]p?

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: p U false

You are quite right. That's indeed a mistake.
Thanks for catching that!