合金中的預定義設置

-1

我在學習合金規格。郎。。我找不到解決問題的方法。我的問題與預定義的元素數有關。合金中的預定義設置

theater_seat集應該有4個成員。觀衆集應該有10個成員。

有一個劇院，只有4個座位可用。但有10個人想看劇院。他們中只有4人可以擁有席位。其餘的將回到家中。我有麻煩了。你能幫我解答一下嗎？

在此先感謝。

編輯

這裏是我的代碼：

module Example 
sig Audiance{ 
    result: lone Seat 
} 

some sig Seat {} 

pred validassignment { 
    '#'Seat=4 
    '#'Audiance=10 
    all a:Audiance | lone a.result 
} 

run validassignment

編輯

我怎樣才能消除這個問題？（在相同的座位就座）

問候

來源

2014-10-10 stackalreadyoverflowed

您可能希望向我們展示你已經做到了，並確定你是否完全卡住位置。對這個模糊問題的模糊回答是：「以聲明方式」思考。

編輯

這不適合，原因有二：

首先，你寫的是語法錯誤。基數運算符是＃和而不是'＃'。（我將您重定向到那裏：http://www.monperrus.net/martin/alloy-quick-ref.pdf爲主要概念很好的概述和合金相關聯的語法），當你運行一個命令是3含義由簽名定義每組

然後，默認的範圍將有一個基數至多3. 因此您需要在您的情況下增加您的範圍爲了找到相關的情況。

您可以指定直接在範圍座椅和audiances數如下：

run validassignment for exactly 4 Seat, exactly 10 Audiance

還有在模型中的其他問題。在目前的狀態下，觀衆中的每個人都可以坐在同一個座位上。我猜你不希望發生這種情況。

祝你好運

來源

2014-10-10 07:48:10

我該如何消除這個問題？（坐在同一座位上） – stackalreadyoverflowed 2014-10-10 11:45:08

加約束 – 2014-10-10 11:50:48

感謝您的幫助 – stackalreadyoverflowed 2014-10-10 12:40:51

合金中的預定義設置

回答

相關問題