出于好奇，我写了一个关于“断言”的奇怪的合金演示。最后，我设置了一个“断言”，对于所有的“程序”，“程序”中的“品种”的所有“值”都是"data1“。我认为“断言”满足“事实”，但是当我检查“断言”时，它给出了一个<
浏览 45提问于2020-06-03得票数 0
回答已采纳
1回答
因此，我创建了一堆合金签名、谓词和事实。我表达了很多关系。我用英语写了一些代表合金模型的陈述：
然后我创建一个合金断言。没有发现反例。正确的英文声明是什么？无反例的合金断言是否代表结论(“因此”陈述)？
浏览 0提问于2018-11-01得票数 0
回答已采纳
使用合金创建模型。邀请合金分析器查看是否存在对断言的反例。这是合金可以做到的事情吗？
如果是，你能提供如何创建模型的提示吗？
浏览 2提问于2016-12-21得票数 1
1回答
我第一次运行合金6 (6.1.0)。我已经更新了我的语法，并且没有收到错误消息。但是我经常检查断言(在合金5中是有效的)：这不可能是对的我该怎么办？
浏览 5提问于2022-09-29得票数 0
我刚刚读了一本软件摘要书，并且非常喜欢合金，因为它的目的是。但我想用它来做比预期更多的事情。创造性地思考，我想使用合金在从真实数据推断的模型实例中找到反例(断言检查)。是否可以对您自己的数据实例使用合金化API？我希望底层的API足够模块化，我可以对自己的工作流程进行编码，而不必详细了解整个系统。如果有这方面的例子，我将感谢指点。谢谢。
浏览 1提问于2015-06-29得票数 0
回答已采纳
1回答
这是我的合金代码： books: set Book, // set of the library's booksassert sameBook2Patrons {因此，当使用以下方法检查断言时：
check sameBook2Pat
浏览 3提问于2016-02-20得票数 0
回答已采纳
，大二的莎拉不应该和任何一年级的学生兼容。fact {}assert WhyDoesThisNotHold {}fact {
no f: Freshman
浏览 2提问于2016-10-24得票数 0
回答已采纳
下面是我在macOS上用合金6.1.0测试的最小化合金模型： root : one Root, no disj nr1, nr2 : NonRoot}
“合金”似乎应该能够在以下结构中找到一个小的反例：
parent = none1 1根节点R1非
浏览 7提问于2022-07-24得票数 0
在下面的合金模型中，有三个单例子签名(Tom、John和Barb)。他们扩大了人的范围。还有一种说法说，这个人完全是由汤姆、约翰和巴布组成的。我原以为合金分析器会产生反例，但它没有。为什么？人不是抽象的，所以可能有人不在(汤姆+约翰+巴布)，对吗？奇怪的是，当我从每个子签名中删除“一个”时，Analyzer就会生成一个反例。我很困惑。你能解释一下这里发生了什么吗？
浏览 1提问于2017-01-28得票数 0
回答已采纳
1回答
我试图建模一个数值变量和一个布尔变量之间的关系，在这个关系中，如果数值变量在某个范围内，那么布尔变量就会改变值。我刚接触过合金，很难理解如何对我的范围进行足够的限制，从而产生明显的反例。: Object | o.discrete = True }
由于o.integer是整数值，范围从0到10，它只能是10种不同选择中的一种因此，在
浏览 0提问于2018-09-21得票数 0
回答已采纳
1回答
我正在学习合金，并试图使它找到两个二元关系r和s，这样s等于r的传递闭包，并且s不等于r。我想我可以通过执行以下命令来让合金做到这一点：{ s : Vassert F { not ( some (s-r) and s=^r ) }现在合金4.2无法找到反例，尽管简单的三元素结构将是r = {(V0,V1), (V1,V2)}和s = r + {(V0,V2)}明显的结构。
浏览 0提问于2015-09-08得票数 2
回答已采纳
2回答
在下面的合金模型中，我想检查两个具有Bool字段类型的sig实例的相等性：
active:合金带反例回来，然而在反例中，x_1和x_2在结构上是相等的，但由于某种原因，合金认为它们不相等。A关系与它的价值没有区别，因此基于编程概念的这种区别在这里没有意义。如果两
浏览 7提问于2021-07-21得票数 1
回答已采纳
1回答
如何在合金中赋值？< b.variable_2 all a:ClassA,b:ClassB| isLess[a,b]
现在，当我在a.variable_2中指定一些比b.variable_2更大的值时，我想检查变量的反例，但是我不知道如何在合金中赋值。所以我的问题是当a.variable_2>b.variable_2
浏览 1提问于2019-03-13得票数 0
回答已采纳
1回答
我看到合金分析器中有一个选项，允许递归达到一定的深度(1-3)。会不会有错误或警告，或者这些反例被默默地忽略了？
浏览 0提问于2018-10-18得票数 0
回答已采纳
1回答
我正在学习合金，并尝试为关系创建谓词injective和surjective。我使用以下模型在合金中尝试了这一点：sig B {}
all disj a, a': r.B | no (a.r &) no r: A -> B | injective[r]但是，我在no r上得到了这个错误
分析不能执行，因为它需要更高层次的量化我读过关于s
浏览 0提问于2018-12-15得票数 2
回答已采纳
1回答
当您在Analyzer中执行您的合金代码时，您会得到一些类似于“没有找到反例”的消息。我想提取这条信息。例如，我希望获得包含此消息的.txt文件。有人能帮帮我吗？
浏览 0提问于2015-06-18得票数 0
1回答
也许这是一个愚蠢的问题，但我正在尝试使用Allow来测试FOL公式的等价性。在反模型的情况下，有什么方法可以展示它们吗？但当我在Counterexample中单击时，它会打开一个没有实例的窗口。
浏览 22提问于2019-09-28得票数 1
回答已采纳
我发现自己在试图总结一套自然的东西。在运行一个简单的模型时，我对下面的行为感到困惑。(假设以下代码位于util/自然科学的副本中，因此将导入ord )fun setsum[nums : set NaturalNatural {}
然后，在一个模块中导入util&
浏览 2提问于2013-09-11得票数 0
回答已采纳
1回答
合金api溶液集
、、
我用合金写了一个简单的模型：sig Password {}
login: one Login all u:User | one u.login.email}
如果我用合金分析仪GUI运行这个程序，它会说：
但是，如果我在java程序中使用API运行相同<em
浏览 5提问于2016-06-20得票数 0
回答已采纳
云服务器
ICP备案
对象存储
实时音视频
云直播
腾讯云开发者
