2016-11-27 4 views

答えて

1

ただ1つのプロセスを1つの場所に追加して、すべてのグローバル不変量をその上に置きます。

宣言:不変

typedef int[1,5] id_t; 
clock c[id_t]; // clocks 
const int b[id_t] = { 10, 20, 30, 40, 50 }; // bounds 

forall(i:id_t) c[i]<=b[i] 

また、境界の配列、例えばを持つことができます

関連する問題