Правда ли, что в NuSMV нет таких значений, как NULL, nil, None?
И что мы не должны создавать модели процесса, потому что модели должны представлять собой электронные схемы?
Мой сценарий заключается в том, что у меня есть один разъем UART, основная память и процесс, в котором последний читает и пишет в основную память, а также читает и пишет в UART. В основной памяти есть данные с именем K, которые должны остаться прежними. Мы хотим доказать, что если процесс не записывает в K' then the value ofK`, то это равно его следующему значению.
Интересно, достаточно ли детализирована моя модель или она слишком абстрактна? Также, если я использовал правильные типы данных.
MODULE UART (proc, output, input)
VAR state : {idle, receive, transmit};
Rx : unsigned word [ 8 ]; --vector of bytes
Tx : unsigned word [ 8 ];
ASSIGN
next (Rx) :=
case
proc = read : input; TRUE : (Rx);
esac;
next (Tx) :=
case
proc = write : output; TRUE : (Tx);
esac;
next (state) :=
case
proc = write : receive; proc = read : transmit; TRUE : idle;
esac;
TRANS
proc != read -> next (Rx) = Rx;
MODULE MEM (proc, input, output)
VAR K : unsigned word [ 8 ]; data : array 0 .. 7 of array 0 .. 7 of unsigned word [ 8 ];
ASSIGN
init (data[1][0]) := K;
next (K) :=
case
output = data[1][0] : output;
TRUE : K;
esac;
MODULE main
VAR proc : {idle, read, write}; input : unsigned word [ 8 ];
output : unsigned word [ 8 ];
memory : MEM (proc, input, output);
uart0 : UART (proc, input, output);
ASSIGN init (input) := memory.data[0][0]; init (output) := memory.data[0][0];
LTLSPEC G (output != memory.data[1][0]) -> G (memory.K = next (memory.K))
