0

我有一个合金模块

module WorkPlace

sig String{}

sig person{}

sig Employee extends person{

name :String, boss: Employee,worker: set Employee}

sig Employee1 extends person{

name :String, boss: Employee,worker: set Employee}


fact Employee{

all e1:Employee, e2:Employee| (e1.name = e2 && e2.name = e1) =>e1 = e2}

run{}

当我三合会运行此模式时，它给了我这个消息：“第 2 行第 5 列的语法错误：此处可能出现 3 个可能的标记：NAME seq this”

不知道是什么意思？

2\ 如果我有 2 个合金模型，每个模型都有相同的元素，即 mode1/name、model2/name。如何创建一个可以说 mode1/name = model2/name 的事实或 pred？

问候

4

1 回答 1

1

  1. 由于 user1513683 已经回答：

    “字符串”是保留字。改用“字符串”（或者，更好的是，“名称”）

  2. 您可以从另一个模块打开现有模块，然后在该模块中您可以使用两个模块中的任何一个中存在的所有签名/关系。例如：

模块 1（文件 m1.als）：

module m1

sig S1 {}

模块 2（文件 m2.als）：

module m2

open m1

sig S2 {}

run { #S1 = #S2 }
于 2013-01-16T16:53:18.693 回答