model - リンクされたリストのモデルチェック

Question

SPINモデルチェッカーで調べました。ただし、動的割り当ての機能はありません。動的割り当てに使用できるモデル チェッカーは他にありますか?

Answer 1

動的割り当ては、さまざまな方法で実現できます。それらのすべてで、割り当て数に上限を設定する必要があります (これは通常、制限要因ではありません)。

割り当てたいものの構造型を定義し、これらの数を配列に入れます。その配列へのインデックスを使用して、構造を参照します。だから、このようなビット：

#define data_t byte

typedef data_record {
  data_t me;
  bool allocated;
  // .... your data fields here ....
}

#define NUMBER_OF_DATA_RECORDS 10

data_record data_record_array[NUMBER_OF_DATA_RECORDS];

#define DATA_RECORD_ALLOCATED(dt)    data_record_array[(dt)].allocated
#define DATA_RECORD_ME(dt)           data_record_array[(dt)].me

inlinesこれで、これらを割り当てて解放するためにいくつかを定義できます。いくつかのオプションがあります。たとえば、割り当てるには、反復して ではないdata_record_arraya を見つけます。このようなビット：data_recordallocated

// Assigns data_ptr with a free data_record index
inline data_record_allocate (data_t data_ptr)
{
   data_ptr = 0; 
   do
   :: data_itr >= NUMBER_OF_DATA_RECORDS -> break
   :: else ->
        if
        :: ! DATA_RECORD_ALLOCATED (data_itr) -> 
           DATA_RECORD_ALLOCATED (data_itr) = true
           DATA_RECORD_ME (data_itr) = data_it
           break
        :: else -> data_itr++
        fi
   od
 }

そして無料は次のようなものです：

inline data_record_free (data_t data_ptr)
{
  DATA_RECORD_ALLOCATED (data_itr) = false
  data_itr = NUMBER_OF_DATA_RECORDS
}

もう少し洗練された方法は、最初はすべてのインデックスであるすべてのフリー インデックスを「フリー インデックス」のチャネルに入れることです。割り当てるときは、チャネルから読み取るだけです。解放したら、チャンネルに押し戻します。