问题标签 [event-b]

我想知道是否可以在event-b中仅使用一个lambda表达式生成一系列素数。这是我到目前为止所拥有的：

@axm1生成一组素数，@axm2定义序列的类型并将@axm3该集合进一步约束为确定性解决方案。我不知道如何用一个 lambda 表达式来做到这一点，我认为这甚至不可能，但我想知道其他人的想法。

我有一个问题如下：

一个小学班级包含许多孩子和各种书籍。编写一个模型来记录孩子们读过的书。它应该保持儿童和书籍之间的关系hasread。

所以我有我的背景

而我的机器如下：

readBooks ∈ students → ℕ 出现错误。显然我在建模这个错误。任何机构都可以帮助我吗？我是事件 B 的新手，我真的不知道该怎么做

我有一个问题如下：

一个小学班级包含许多孩子和各种书籍。编写一个模型来记录孩子们读过的书。它应该保持儿童和书籍之间的关系hasread。它还应该处理以下事件：

记录：添加给定孩子已阅读给定书籍的事实

newbook：输出给定孩子尚未阅读的书

books_query：输出给定孩子已阅读的书籍数量

到目前为止，这是我的模型

而我的机器如下：

我有一个活动，我想将给定学生的书标记为已读。它有两个参数：学生姓名和书名。

现在看守卫。我想说

我有这个，但不工作，我不知道现在该怎么办。谁能帮我

我是 Event-B 的初学者，我正在尝试建模一台机器，其中集合 PERSONNE 包含集合 CLIENT，集合 CLIENT 包含集合 RESIDENT ...我已经搜索了罗丹的文档，但我没有找到任何东西。 . 这是上下文

这是机器

我想我有这个想法，但我无法解决我得到的各种错误：类型 CLIENT 和 PERSONNE 不匹配（3 次） 类型 RESIDENT 和 CLIENT 不匹配（2 次）......

我在使用 Event-B 时遇到了很多麻烦。

我想将一组客户与每个客户编号建立关系

我有这种类型的关系：

cli(PERSON) = NAT1 （人是有限集）

如果我有一部分人

我想影响 cli 关系我会直观地写什么：

我是否以正确的方式建模？有什么方法可以得到我想要的矫揉造作吗？

给定一些条件，我想检查变量下一个状态是否适用于某个命题。我无法创造出罗丹接受的东西。

我的确切情况是以下不变量。我想确保door当锁打开时变量永远不会改变。变量door是Open或者Closed

如果PrimaryLock是On这意味着无论接下来触发什么事件，门的状态都不会改变。

这可以使用 Event-b 还是我需要通过添加其他变量来解决我的问题？

我在ProB中可视化大量代码时遇到问题。此图显示了带有（使用 Graphviz dotty）ProB 的服务器的登录部分，但没有解决大量代码获取该图的解决方案。请让我知道您的建议和想法，

我在事件 B 中遇到了解除证明义务的问题。在我的工作中，我想将内存保护要求的规范形式化，以检查它们之间的一致性。为此，我使用 Event-B Context 来形式化系统的结构，并使用 Event-B Machine 来描述需求。每个需求都在 Invariant 和 Event 中进行了描述。Event-B 将检查每对需求以发现不一致之处。
但是，它不能证明两个要求是一致的： 1：“ NonTrusted对其他 OS_App的data_section 的读取访问权限是may_prevent ” 2：“来自OS_App的读写访问权限
对其自己的 data_section是shall_permit "

这是我的工作。首先，在上下文文件中，我描述了系统的结构和访问控制：
1. 系统的结构：
我们有两种类型的 OS_Application：Trusted和NonTrusted。
2 种 OS_Objects：Tasks和ISRs。
2 种 ISR：Category_1和Category_2。
每个 OS_Object 属于一个 OS_App：ContainerOf ∈ OS_Obj → OS_App
每个 OS_App 都有一个代码段：AppCode ∈ OS_App → CodeSection
内存有 2 个部分：DataSection和Stack
OS_App 和 OS_Obj可能有 DataSection：

• AppData ∈ OS_App ⇸ DataSecs
• ObjData ∈ OS_Obj ⇸ DataSecs

OS_Obj 有自己的 Stack：ObjStack ∈ OS_Obj → Stacks

2.访问控制：
访问是从Subjects到Objects：
Subjects包括：OS_App和OS_Obj
Objects包括：Code_Section和Memory
在下面的代码中，第20行描述：“这些对象的堆栈，根据定义，只属于所有者对象，因此不需要在对象之间共享堆栈数据，即使这些对象属于同一个操作系统应用程序。”

第 21 行描述：“代码部分是 OS 应用程序私有的，或者可以在所有 OS 应用程序之间共享”
第 22、23 行描述：“OS 应用程序可以有私有数据部分，而任务/ISR 可以有私有数据部分。 "
第 24 行描述：“操作系统应用程序的私有数据部分属于该操作系统应用程序的所有任务/ISR 共享。”

通过分析，我将上下文定义如下：

其次，在机器文件中，我描述了：

以及两个事件：两个事件
之后，事件-B 生成 Proof Obligations 并尝试证明一致性。但是，这两个要求是不一致的，如下： undischarged Proof Obligation
In the Goal box：它不能证明：
A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)))是真的。
但是，在要求 2 中，我们有：app1 ≠ app2
=> app ≠ app2 (because app1=app) =>AppData(app2) ≠ AppData(app) 因此，(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)= FALSE
然后 A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)))= TRUE。

请给我一些提示或评论好吗？

我在我最新版本的罗丹平台中导入了一个完全精炼的模型，我正在尝试在这个项目中使用带有 ProB 动画师的 IUMLB。但由于该项目已经有一个预配置的 AnimB 动画师，最新的罗丹软件不支持。错误状态为“未知配置 org.animb.valuation.valBase”。

如何从项目中删除或修复此 AnimB 配置？

我有如下问题：A定义了一个集合并且X具有不变类型的总函数

和一个事件A_setSate：

问题是证明义务事件保存（INV）A_setState不能保存不变量X∈ A--> BOOL：

我知道这是因为不变量不够强，但我无法创建更强的不变量。

完整示例：示例截图