个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
26
4
我很难理解 Alloy 4 中谓词和函数之间的区别。我已经阅读了软件抽象中的第 4.5.2 节，但我仍然不清楚。谁能帮我理解一下？
最佳答案
一个函数只是代表一个参数化的表达式，它在每个调用站点被内联。
谓词代表一个公式，即一个 bool 表达式，所以从这个意义上说，它有点像一个返回 bool 表达式的函数。另一个区别是，在 Alloy 中，您可以使用 Alloy 的“运行”和“检查”命令来“运行”和“检查”谓词。运行谓词指示 Alloy 查找该谓词适用的模型，而检查谓词指示 Alloy 检查是否存在该谓词不适用的模型。
关于alloy - 合金 4 中函数和谓词的区别？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/16466971/
26
4
0
是否可以在 Alloy 中模拟随机故障？ 例如，我目前有一个连通图，它在不同的时间步将数据传递给它的邻居。我想做的是找出一些允许模型随机终止链接的方法，并且在这样做的过程中，仍然设法实现其目标(确保所
来自 this question 的跟进... 我有一个完全连接的图，这很棒。我还添加了时间的概念。我现在正在为围绕我的图表传递数据的概念而苦苦挣扎。 我正在建模一个系统，该系统的任务是确保每个节点都
我正在关注 Daniel Jackson 的优秀著作 (Software Abstractions)) 中的一个示例，特别是他设置 token 环以选举领导者的示例。 我正在尝试扩展此示例( Ring
我正在使用 # 运算符来获取笛卡尔积 (A->B) 和并集 (A+B) 的基数。但它返回奇怪的负数，我不知道它们是什么!？ 请查看下面的快照，其中显示了我的模型的 A->B 和 A+B 内容以及 Al
在 Alloy 书籍第 4.7.2 节的以下代码中， 是什么意思？这个关键字指的是？ module library/list [t] sig List {} sig NonEmptyList exte
我对使用 Alloy 的 String 类型很感兴趣(特别是因为它允许使用特殊字符)。我注意到，为了将给定的字符串添加到实例中，将其包含在表达式中就足够了。例如 fact stringInsert{
我在学习 Alloy 时获得了很多乐趣，并且很高兴将它应用到我正在从事的一些软件项目中。 过去，我曾非正式地使用轻量级形式化方法(如果是的话)，以一阶逻辑编写我期望系统具有的一些不变量。我从来没有用它
这里的任何人都可以解释传递闭包运算符如何根据矩阵在 Alloy 中工作。我的意思是将闭包运算符转换为实际矩阵运算的转换规则是什么。 最佳答案 为了计算传递闭包，Kodkod 使用迭代平方。 简而言之，
我开始学习合金并且非常喜欢我所看到的。 在鼓励同事和我一起学习和使用 Alloy 之前，我需要了解 Alloy 和 UML 之间的关系。 Alloy 是 UML 的替代品吗？如果用Alloy，那就不用
我想知道是否有人在 Alloy 中完整指定了 Alloy 语言。 如果存在这样的元模型，它是否公开可用？ 最佳答案 您的意思是您想要像 http://docs.appcelerator.com/tit
我在 avlTree.als 中有一个合金模型。该模型使用整数算术，特别是加号和减号函数。该模型中有一些断言，我可以使用合金分析器 GUI 很好地运行这些断言。 我在 test.als 中有另一个合金
下面是两个桌面的 Alloy 表示。在 fact 中，我指定第一个桌面包含两个图标 A 和 B，第二个桌面包含一个图标 A。我想指定正好有两个桌面，所以我将事实上: #Desktop = 2 当我执行
我想引用可以在这个地址找到的问题: Running alloy analyzers in parallel 是否有关于合金模型分解的持续研究或结论，以便对模型进行更优化的分析？ 这让我很感兴趣。 最佳
假设我有以下签名: sig A {} sig B {} sig P { a: A, b: B } 我如何编写一个函数 f，例如，f 返回 P 的集合，其中每个成员的值为 x: A 表示
CompUtil.parseOneExpression_fromString 方法给出以下错误:无法找到名称“Atom$0” 当解析的字符串包含表达式时直接包含原子的标签。 这是可以理解的，因为单独的
在 the Alloy grammar spec在 Alloy 网站上，我发现自己对方括号的使用感到困惑。 在如下所示的制作中，事情似乎很清楚。 specification ::= [module]
假设我的模块中有一个与 sig B 相关的 sig A。 想象一下，现在我们有几个实例: A$1 -> B$1 , A$2 -> B$2 和 A$1 -> B$2 , A$2 -> B$1 我
合金中是否有异或运算，如果没有，我该如何定义它: 我想要一个名为 xor 的谓词，它以两个谓词作为参数，并且当它们的 xor 为真时它也为真。 更详细地说，如果我有 P1 和 P2，我知道我可以将 P
这是家庭作业，我遇到了很多麻烦。我正在使用 Alloy为图书馆建模。下面是对象的定义: sig Library { patrons : set Person, on_shelves :
我有一个合金模型，它有 2 个签名，它们有一个同名的关系。 sig Model { components : set Component } sig Port extends Element
我是一名优秀的程序员,十分优秀！