nuXmv как он узнает в исходном состоянии, что (AF p) & (AF w) ложно - PullRequest
Новая
       67

nuXmv как он узнает в исходном состоянии, что (AF p) & (AF w) ложно

0 голосов
/ 07 мая 2018

У меня есть вопрос, касающийся решения nuXmv. У меня есть простой график, где начальное состояние s1 и есть две дуги от s1, одна ведет к s2, другая к s3. Из s2 и s3 есть одна дуга, ведущая к s1. Это программа в nuXmv, которая описывает ситуацию. 

MODULE main
VAR
    s : {s1, s2, s3};  
    p : boolean;
    q : boolean;
    w : boolean;
ASSIGN 
    init(s) := {s1};
    next(s) := case 
        s = s1 : {s2, s3}; 
        s = s2 : s1;
        s = s3 : s1;
    esac;
    p := case 
        s = s2 : TRUE;
        TRUE : FALSE; 
    esac;
    q := case
        s = s1 : TRUE;  
        TRUE : FALSE; 
    esac;
    w := case
       s = s3 : TRUE;
        TRUE : FALSE;
    esac;
CTLSPEC (AF p) & (AF w);
CTLSPEC AG (AF p) & AG (AF w);

Я не понимаю, как nuXmv уже в исходном состоянии s1 знает, что формула неверна. Он не дает контрпример на основе цикла, просто сразу в s1 он говорит, что формула неверна на основе s1. Моя идея объяснения состоит в том, что без допущений справедливости nuXmv немедленно предполагает, что один из путей никогда не может быть выполнен. Но не должно ли это привести цикл в качестве примера? Если бы я только оставил "CTLSPEC AF p;" nuXmv возвращает цикл как контрпример. Так почему же для «AF p & AF w» в качестве контрпримера показывается только состояние s1? 

-- specification (AF p & AF w)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    s = s1
    p = FALSE
    q = TRUE
    w = FALSE
...