638
edits
m (→Thread state expressions: formatting) |
|||
| Line 129: | Line 129: | ||
A thread state expression is '''inconsistent''' if it's self-contradictory, like "(P AND NOT P)". This means this thread state expression can never be satisfied; it's never true. Note that "((P AND NOT P) OR Q)" is not inconsistent; it simplifies to "Q". | A thread state expression is '''inconsistent''' if it's self-contradictory, like "(P AND NOT P)". This means this thread state expression can never be satisfied; it's never true. Note that "((P AND NOT P) OR Q)" is not inconsistent; it simplifies to "Q". | ||
One thread state expression may '''imply'' another, as in logic: "(P AND Q)" implies "(P OR R)". It means any time the former is true, the latter will be true. | One thread state expression may '''imply''' another, as in logic: "(P AND Q)" implies "(P OR R)". It means any time the former is true, the latter will be true. | ||
=== Known thread state === | === Known thread state === | ||
edits