0
すべての状態が指定された時間より長くならないように指定したいと思います。私はそれを州ごとに指定することでそれをすることができますが、人間はそれを忘れることができます。私はグローバルな解決策が必要です。私は、「各州の最大時間」のようなものを意味します。UPPAALグローバルの各状態に最大時間を指定する方法はありますか?
すべての状態が指定された時間より長くならないように指定したいと思います。私はそれを州ごとに指定することでそれをすることができますが、人間はそれを忘れることができます。私はグローバルな解決策が必要です。私は、「各州の最大時間」のようなものを意味します。UPPAALグローバルの各状態に最大時間を指定する方法はありますか?
ただ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]
また、境界の配列、例えばを持つことができます