Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
| pn2mc:pt_cp_model_checking [2014/11/24 23:43] jbiernacki [nuXmv] | pn2mc:pt_cp_model_checking [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 179: | Line 179: | ||
| < | < | ||
| - | NuSMV > check_ltlspec | + | nuXmv > check_ltlspec |
| -- specification G ( F p5) is false | -- specification G ( F p5) is false | ||
| -- as demonstrated by the following execution sequence | -- as demonstrated by the following execution sequence | ||
| Line 218: | Line 218: | ||
| -- specification G (((((!p0 & !p1) & !p2) & !p3) & !p4) -> ((((p5 | p6) | | -- specification G (((((!p0 & !p1) & !p2) & !p3) & !p4) -> ((((p5 | p6) | | ||
| p7) | p8) | p9)) is true | p7) | p8) | p9)) is true | ||
| - | NuSMV > check_ctlspec | + | nuXmv > check_ctlspec |
| -- specification EF p5 is true | -- specification EF p5 is true | ||
| -- specification EF p6 is true | -- specification EF p6 is true | ||
| Line 361: | Line 361: | ||
| - | To verify specified properties of the system, the following LTL and CTL formulae were created: | + | To verify specified properties of the system, the following LTL formulae were created: |
| - Consumer do not try to receive data from empty buffer, \\ \\ '' | - Consumer do not try to receive data from empty buffer, \\ \\ '' | ||
| Line 382: | Line 382: | ||
| < | < | ||
| - | NuSMV > check_ltlspec | + | nuXmv > check_ltlspec |
| -- specification ( G ( F P4_client = 1) -> G ( F P5_client = 1)) is true | -- specification ( G ( F P4_client = 1) -> G ( F P5_client = 1)) is true | ||
| -- specification ( G ( F P2_factory = 1) -> G ( F P1_factory = 1)) is true | -- specification ( G ( F P2_factory = 1) -> G ( F P1_factory = 1)) is true | ||