Как сделать неинициализированную переменную в Spin?

Question

Кажется, что Promela инициализирует каждую переменную (по умолчанию, 0 или значение, указанное в объявлении).

Как я могу объявить переменную, инициализированную неизвестным значением?

документация предполагает if :: p = 0 :: p = 1 fi, но я не думаю , что он работает: Спин по-прежнему проверяет это утверждение

bit p 
init { if :: p = 0 :: p = 1 fi } 
ltl { ! p } 

(и фальсифицирует p)

Так что же семантика init? Есть еще «предварительное начальное» состояние? Как я могу обойти это - и не путать моих учеников?

Answer 1

Это интересный вопрос.

В документе documentation указано, что каждая переменная инициализируется до 0, если только модель не указала иначе.

Как и во всех объявлениях переменных, явное поле инициализации является необязательным. Начальное значение по умолчанию для всех переменных равно нулю. Это относится как к скалярным переменным, так и к переменным массива, и применяется как к глобальным, так и к локальным переменным.

В вашей модели, вы не инициализирует переменную при объявлении его, поэтому он впоследствии присваивается значение 0 в исходном состоянии, которое находится перед вашим назначением:

bit p 

init { 
    // THE INITIAL STATE IS HERE 
    if 
    :: p = 0 
    :: p = 1 
    fi 
} 

ltl { ! p } 

---

Некоторые эксперименты.

«наивным» идея уворачиваясь это ограничение было бы изменить гр исходного кода из pan.c, который генерируется спина при вызове ~$ spin -a test.pml, так что переменная инициализируется в случайном порядке ,

Вместо этой функции инициализации:

void 
iniglobals(int calling_pid) 
{ 
     now.p = 0; 
#ifdef VAR_RANGES 
     logval("p", now.p); 
#endif 
} 

можно попробовать написать так:

void 
iniglobals(int calling_pid) 
{ 
     srand(time(NULL)); 
     now.p = rand() % 2; 
#ifdef VAR_RANGES 
     logval("p", now.p); 
#endif 
} 

и добавление в части заголовка в #include <time.h>.

Однако после того, как вы собираете, что в верификатор с gcc pan.c, и вы пытаетесь запустить его, вы получите недетерминирована поведения в зависимости от значения инициализации переменной р.

Это может как определить, что свойство нарушается:

~$ ./a.out -a 
pan:1: assertion violated !(!(!(p))) (at depth 0) 
pan: wrote test.pml.trail 

(Spin Version 6.4.3 -- 16 December 2014) 
Warning: Search not completed 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    + (ltl_0) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

State-vector 28 byte, depth reached 0, errors: 1 
     1 states, stored 
     0 states, matched 
     1 transitions (= stored+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.291 actual memory usage for states 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    128.730 total actual memory usage 



pan: elapsed time 0 seconds 

или печати, что свойство выполнено:

~$ ./a.out -a 
(Spin Version 6.4.3 -- 16 December 2014) 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    + (ltl_0) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

State-vector 28 byte, depth reached 0, errors: 0 
     1 states, stored 
     0 states, matched 
     1 transitions (= stored+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.291 actual memory usage for states 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    128.730 total actual memory usage 


unreached in init 
    test.pml:8, state 5, "-end-" 
    (1 of 5 states) 
unreached in claim ltl_0 
    _spin_nvr.tmp:8, state 8, "-end-" 
    (1 of 8 states) 

pan: elapsed time 0 seconds 

Очевидно, что начальное состояние модели Promela проверена по спин считается уникальным. В конце концов, это разумное предположение, поскольку оно без проблем осложняло бы вещи: вы всегда можете заменить N разных начальных состояний S_i начальным состоянием S s.t. S позволяет достичь каждого S_i с эпсилон-переходом. В этом контексте то, что вы получаете, не является действительно эпсилон-переходом, но на практике это мало чем отличается.

EDIT(с комментариями): В принципе, можно сделать эту работу путем модификации pan.c немного дальше:

• преобразовать начальное состояние Инициализатора в генератор начальных состояний
• изменить процедуру проверки, чтобы учесть, что m руды чем одного исходного состояния может существовать, и что свойство должно выполняться для каждого начального состояния

Сказав это, вероятно, не стоит этого делать, если это не будет сделано, исправляя Спин «s исходный код.

---

Обход проблемы.

Если вы хотите сказать, что что-то верно в исходном состоянии, либо исходя из начального состояния, а также принимать во внимание некоторые недетерминированное поведение, то вы должны написать что-то выглядит следующим образом:

bit p 
bool init_state = false 

init { 
    if 
    :: p = 0 
    :: p = 1 
    fi 
    init_state = true // TARGET STATE 
    init_state = false 
} 

ltl { init_state & ! p } 

, с которым вы получите:

~$ ./a.out -a 

pan:1: assertion violated !(!((initialised& !(p)))) (at depth 0) 
pan: wrote 2.pml.trail 

(Spin Version 6.4.3 -- 16 December 2014) 
Warning: Search not completed 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    + (ltl_0) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

State-vector 28 byte, depth reached 0, errors: 1 
     1 states, stored 
     0 states, matched 
     1 transitions (= stored+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.291 actual memory usage for states 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    128.730 total actual memory usage 



pan: elapsed time 0 seconds 

---

Init семантику.

Иниц просто гарантированно будет первый процесс, чтобы порождать, и предназначается, чтобы быть , используемый для порождения других процессов когда,-например, другие процедуры принимают в качестве ввода некоторых параметров, например некоторые ресурсы разделяются. Больше информации here.

Я считаю, что этот фрагмент documentation немного вводит в заблуждение:

Процесс инициализации обычно используется для инициализации глобальной переменной с, и создания экземпляров других процессов, за счет использования пробега , перед запуском системы. Любой процесс, а не только процесс первонач, может сделать это, хотя

Так можно гарантии, что процесс инициализации выполняет все его кода перед любым другим способом с помощью atomic { } заявление, можно сказать, что его можно использовать для инициализации переменных до того, как они будут использоваться другими процессами с с точки зрения программирования. Но это всего лишь приблизительное приближение , потому что процесс init не соответствует уникальному состоянию в модели исполнения, а скорее дереву состояний у корня, а сам корень предоставляется только в глобальной среде , как и перед началом любого процесса.