合金中的预定义设置

-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

合金中的预定义设置

回答

相关问题