Spinroot

A forum for Spin users

You are not logged in.

#1 2019-06-02 09:46:57

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?

Offline

#2 2019-06-04 19:31:05

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: p U false

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

Offline

Board footer

Powered by FluxBB