使用 Alloy API 生成与模型实例对应的 .als 文件 [英] Generating .als files corresponding to model instances with Alloy API

问题描述

假设我有以下模型:

sig counter{
value: Int,
}
{
 value > 0
 value < 3
}
pred show{}

run show for exactly 1 counter

我想生成与此模型的两个实例对应的 als 文件:

I would like to generate the als files corresponding to the two instances of this model :

open counter 
one sig counter_1 extends counter{}{ value=1 }   
fact { counter = {counter_1}}

和，

open counter 
one sig counter_2 extends counter{}{ value=2 }   
fact { counter = {counter_2}}

我已经使用 Alloy API 来生成实例，但我找不到将它们导出到 als 文件的方法(除非解析 xml 或 txt 文件).

I have used the Alloy API to generate the instances but I cant find the method to export them to als files (unless parsing xml or txt files).

我可以想象有这样一种方法，特别适用于进行模型转换的人(这是我的情况，因为我想将实例转换回原始元模型)

I can imagine there exist such a method especial for people who do model transformation (which is my case since I want to transform the instances back to the original méta model)

有什么提示吗?谢谢

推荐答案

去你电脑里的这个地方

C:\Users\'用户名'\Desktop\alloy4.2\models\util

C:\Users\'the name of user'\Desktop\alloy4.2\models\util

，你会发现这里保存了很多.als文件.下一步将您的文件保存在那里.

, you will find there are a lot of .als files that are saved here. next step save your file there.

但是...尝试将计数器保存在您将创建第二个的同一个文件夹中.我已经解决了您在此处附加的所有示例.

but... try to save the counter in the same folder that you will create the second one. I had solved all the examples that you attached here.

> module Counter
> 
> sig counter{ value: Int, } {  value > 0  value < 3 } pred show{}
> 
> run show for exactly 1 counter

这是您的第一个示例:

  module test 
 open counter   
one sig counter_1 extends counter{}{ value=1
  }    fact { counter = {counter_1}}

这是你的第二个例子:

module test2
open counter 
one sig counter_2 extends counter{}{ value=2 }   
fact { counter = {counter_2}}

这篇关于使用 Alloy API 生成与模型实例对应的 .als 文件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！