我是Alloy的初学者 . 这是我使用Alloy Analyzer的第一个型号 . 我现在正在为合金旅行建造一个通用模型 . 在此模型中，用户（我在此模型中使用sig请求）可以请求“住宿”（包括“酒店”或“公寓”或“宿舍”）; '飞行';或“游览”，（请求可以是其中之一，也可以是它们的任意组合，例如酒店和旅游） . 它们中的每一个都是“资源”的子集 . 目前，我只支持一个目的地的请求，住宿的入住和退房日期以及航班的入境日期和出境日期必须与用户请求的开始日期和结束日期相同 .
我的问题如下：
-
首先，为了确保办理登机手续，退房，入境和出境日期与用户请求的开始日期和结束日期相同，所有这些都映射到beginning_of_journey和end_of_journey（请参阅代码） . 这是正确的方法吗？
-
其次，我对如何编码约束有疑问 - 游览日期必须在用户请求的开始日期和结束日期之内（因此游览日期必须在登记入住，入站，退房和出境之内）约会） . 我定义了一个设置日期（sig日期），其中包含字段日，月和年，其中每个字段都被定义为整数 . 但问题是天数可以是负数 . 在执行代码之后，给定的实例看起来很奇怪 . 任何人都可以提出建议或建议我定义这种约束的正确方法吗？
-
第三，我有一个需要澄清的问题 . 假设上述问题已经解决，我需要初始化具体请求，例如旅行日期是2016年7月1日，日期开始时间是2016年7月2日，结束日期是2016年7月4日 . 因为我有定义了上述约束（问题2），我希望Alloy告知违反了给定的日期 . 合金有可能做到这一点吗？
如果有人能提出一些意见和建议，我将非常感激 . 谢谢
1 回答
您需要测试相同性和订单的日期 . 但是，除非您试图检查设计的正确性以计算公历中日期的相同性和顺序，否则合金中日期的内部结构建模似乎没什么用处 .
所以在你的位置上，我会像LoïcGammaitoni已经建议的那样，在Date上定义一个排序，以支持你对序列的查询 .