Generating .als files corresponding to model instances with Alloy API

Question

suppose I have the following model :

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

run show for exactly 1 counter

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}}

and,

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

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)

Any hints? Thanks

score 0 · Answer 1 · answered Dec 25 '19 at 19:07

0

I do not think there is a way to do this easily. There is a pkriens/api branch that provides and API that would make it easier to export this since you can get the solution as easy to use API objects.

answered Dec 25 '19 at 19:07

Peter Kriens

15,196
1
37
55

score 0 · Answer 2 · answered Dec 26 '19 at 20:03

0

It seems that you already have .als files that match your description; they are given in the second and third code blocks of your question.

What am I missing? (Or, not quite the same thing, what requirements are missing from your question?)

answered Dec 26 '19 at 20:03

C. M. Sperberg-McQueen

24,596
5
38
65

those files are what he desires to generate automatically – Loïc Gammaitoni Jan 02 '20 at 08:05

score 0 · Answer 3 · answered Jan 02 '20 at 08:45

0

We had the same needs when developing Lightning, we called that "instance promotion".

To implement instance promotion, we developed an algorithm that consisted in going through the A4Solution generated (see going through an A4Solution) and generating for each element some Alloy code that would then be persisted into an .als file.

I will try to put the source code of the tool online. Worst case, you'll have to redo it from scratch, it won't be too hard I believe.

answered Jan 02 '20 at 08:45

Loïc Gammaitoni

4,173
16
39

Ok. Thanks. Please let me know if you put the code online. – Abdelghani Jan 07 '20 at 15:43
Code will remain offline as it is now the IP of the university. I didn't bother to copy the source at the time. Silly me ... – Loïc Gammaitoni Dec 18 '20 at 12:49

score 0 · Answer 4 · answered Jan 17 '20 at 14:47

go to this place in your computer

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

, 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

this is your first example:

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

and this is your second example:

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

Generating .als files corresponding to model instances with Alloy API

4 Answers4

Linked