Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
709
stars
124
forks
source link
At tracing abstract signature, I looks like odd ordering #58
open util/ordering[Student]
enum Type { X, Y }
abstract sig Student{
T : Type,
TransHistory: set TransRecord
}
sig StudentX extends Student{
}{
T = X
}
sig StudentY extends Student{
}{
T = Y
}
sig TransRecord{
}
pred init(s: Student){
no s.TransHistory
}
fact traces{
first.init
all s: Student - last | let s' = s.next |
some x: TransRecord |
s'.TransHistory = s.TransHistory + x and s'.T = s.T
}
run {} for 5
I projected about Student and executed tracing, it was traced as 0 -> 1 -> 2 ...
However, when checked in the evaluation environment, it is as follows.
In other words, it became random internally and it seemed that the meaning did not go through as trace.
I understand the reason.
It is because it orders Student and it is not attached to StudentX.
But, then, I think that I want the execution trace to be displayed in order of the student being ordered, and I think that is more reasonable.
My code looks like below.
I projected about Student and executed tracing, it was traced as 0 -> 1 -> 2 ... However, when checked in the evaluation environment, it is as follows.
In other words, it became random internally and it seemed that the meaning did not go through as trace.
I understand the reason. It is because it orders Student and it is not attached to StudentX. But, then, I think that I want the execution trace to be displayed in order of the student being ordered, and I think that is more reasonable.