alloy - 有没有办法找出在合金中运行时导致 'No Instance Found' 的原因？-6ren

alloy - 有没有办法找出在合金中运行时导致 'No Instance Found' 的原因？

转载作者：行者123 更新时间：2023-12-01 09:16:09

25

4

我使用合金在模型中编写。但是，在某些情况下，运行谓词以查找实例失败，并且它表示找不到实例。我尝试将绑定(bind)增加到大约 16 个实例，但它没有找到任何实例。

有什么方法可以调试它，以便我可以看到哪些事实失败导致 Alloy 无法找到实例？

谢谢!

最佳答案

如果您将默认 sat 求解器更改为具有 unsat 核心的 minisat，则可以突出显示在同一实例中无法满足的约束。

另一种可能的解决方案是逐个注释您的约束，直到分析产生一个实例，从而确定哪个约束可能导致问题。

如需更具体的答案，请分享您的模型。

关于alloy - 有没有办法找出在合金中运行时导致 'No Instance Found' 的原因？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/44234264/

25

4

0

文章推荐： chart.js - 如何使用react-chartjs-2创建堆叠的条形图？

文章推荐： ipc - 不断地将事件从主进程传递到渲染进程

文章推荐： python - 检查并删除 python MongoDB 中的重复项

android - 当我们使用 SQLite 时，当我们使用 content provider 时，当我们使用 Shared preference 时
SQLite、Content provider 和 Shared Preference 之间的所有已知区别。但我想知道什么时候需要根据情况使用 SQLite 或 Content Provider 或
Backbone.js 模型验证仅在 set->save 时(不是在 fetch 时)
警告:我正在使用一个我无法完全控制的后端，所以我正在努力解决 Backbone 中的一些注意事项，这些注意事项可能在其他地方更好地解决......不幸的是，我别无选择，只能在这里处理它们! 所以，我的
jquery - 使用 “prefetch” 时 Twitter 预输入没有结果，但使用 “remote” JSON 时
我一整天都在挣扎。我的预输入搜索表达式与远程 json 数据完美配合。但是当我尝试使用相同的 json 数据作为预取数据时，建议为空。点击第一个标志后，我收到预定义消息“无法找到任何内容...”，结果
java - repaint() 时 JTextArea 不显示，但 revalidate() 时 Graphics 不更新？
我正在制作一个模拟 NHL 选秀彩票的程序，其中屏幕右侧应该有一个 JTextField，并且在左侧绘制弹跳的选秀球。我创建了一个名为 Ball 的类，它实现了 Runnable，并在我的主 Draf
java - java中将时间戳转换为特定格式(年、月、周、日、时、时、分、秒)
这个问题已经有答案了: How can I calculate a time span in Java and format the output? (18 个回答) 已关闭 9 年前。这是我的代码
设置 header 时 AJAX 请求失败，但没有设置 header 时 AJAX 请求会成功
我有一个 ASP.NET Web API 应用程序在我的本地 IIS 实例上运行。 Web 应用程序配置有 CORS。我调用的 Web API 方法类似于: [POST("/API/{foo}/{ba
android - 用户输入年、月、日、时、分与系统年、月、日、时、分的区别
我将用户输入的时间和日期作为: DatePicker dp = (DatePicker) findViewById(R.id.datePicker); TimePicker tp = (TimePic
algorithm - 在处理 Tabu Search Optimization 时，当所有相邻解决方案都是 tabu 时，通常的做法是什么？
放宽“邻居”的标准是否足够，或者是否有其他标准行动可以采取？最佳答案如果所有相邻解决方案都是 Tabu，则听起来您的 Tabu 列表的大小太长或您的释放策略太严格。一个好的 Tabu 列表长度是
c++ - 为什么我需要传递一个比较器来构造一个 priority_queue，当它是 lambda 时，而不是当它是 std::greater 时？
我正在阅读来自 cppreference 的代码示例: #include #include #include #include template void print_queue(T& q)
javascript - 当触发器为 'click' 时，Bootstrap 3 工具提示表现得很奇怪，当触发器为 'manual' 时，则不起作用
我快疯了，我试图理解工具提示的行为，但没有成功。 1. 第一个问题是当我尝试通过插件(按钮 1)在点击事件中使用它时 -> 如果您转到 Fiddle，您会在“内容”内看到该函数' 每次点击都会调用该属
javascript - 使用 useContext 时，数据首先加载为空数组，当我应用 .map() 或 .find() 时，我收到一条错误消息
我在功能组件中有以下代码: const [ folder, setFolder ] = useState([]); const folderData = useContext(FolderContex
swift - 使用 NSURLSession 时 GET 成功，但使用 AFHTTPSessionManager 时 GET 失败
我在使用预签名网址和 AFNetworking 3.0 从 S3 获取图像时遇到问题。我可以使用 NSMutableURLRequest 和 NSURLSession 获取图像，但是当我使用 AFHT
java - 当池生命周期为 LIFE_CYCLE_FAILED 时，使用 UCP 管理器调用 closeConnections() 时 UCP 连接是否关闭？
我正在使用 Oracle ojdbc 12 和 Java 8 处理 Oracle UCP 管理器的问题。当 UCP 池启动失败时，我希望关闭它创建的连接。当池初始化期间遇到 ORA-02391:超过
ios - 当我点击 "Run"时，应用程序崩溃，但是当我点击 "Stop"然后 "Run"时，应用程序崩溃
关闭。此题需要details or clarity 。目前不接受答案。想要改进这个问题吗？通过 editing this post 添加详细信息并澄清问题. 已关闭 9 年前。 Improve
css - 我有一个笨蛋。当我在全局范围内定义我的 css 时，它起作用了。当我在我的组件中定义我的 css 时，它失败了。这是怎么回事？
引用这个plunker: https://plnkr.co/edit/GWsbdDWVvBYNMqyxzlLY?p=preview 我在 styles.css 文件和 src/app.ts 文件中指定
python - 当宽度 <1.0 时，Matplotlib 周线太细；当宽度>=1.0 时，周线太粗
为什么我的条形这么细？我尝试将宽度设置为 1，它们变得非常厚。我不知道还能尝试什么。默认厚度为 0.8，这是应该的样子吗？ import matplotlib.pyplot as plt import
当我使用 RIGHT JOIN 时，MYSQL 无法识别字段，但当我使用 NATURAL JOIN 时，MYSQL 可以识别字段
当我编写时，查询按预期执行: SELECT id, day2.count - day1.count AS diff FROM day1 NATURAL JOIN day2; 但我真正想要的是右连接。当
python - 在 pandas 中读取时间值(时、分、秒、日、月、年)时，如何指定先到先得？
我有以下时间数据: 0 08/01/16 13:07:46,335437 1 18/02/16 08:40:40,565575 2 14/01/16 22:2
javascript - 当我使用 axios POST 时，Req.body 为空，但当我使用 'request' 时，它工作正常
一些背景知识 -我的 NodeJS 服务器在端口 3001 上运行，我的 React 应用程序在端口 3000 上运行。我在 React 应用程序 package.json 中设置了一个代理来代理对端
javascript - 使用 AngularJs 时，当 img 标签具有 src attr 时，如何在其上设置 data-src
我面临着一个愚蠢的问题。我试图在我的 Angular 应用程序中延迟加载我的图像，我已经尝试过这个2: 但是他们都设置了 src attr 而不是 data-src，我在这里遗漏了什么吗？保留 d

首页

博学

6Ren·AI

商城

alloy - 有没有办法找出在合金中运行时导致 'No Instance Found' 的原因？