Time — Alloy Documentation documentation
source link: https://alloy.readthedocs.io/en/latest/language/time.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Time¶
Alloy 6 added temporal operators to Alloy, making it easier to model dynamic systems.
Variables¶
A signature or relation can be declared mutable with the var
keyword:
sig Server {}
var sig Offline in Server {}
sig Client {
, var connected_to: lone Server - Offline
}
The set of servers that are offline is mutable: different servers can be offline in different steps. The connected_to
field is also mutable and can have different Client -> Server
pairs in different steps.
This uses the in
modifier as in the Subtyping technique.
The number of steps in a model is specified with the Steps command.
Temporal Operators¶
A dynamic model is broken into several Steps. For each step, all var
signatures and relations may change, depending on the predicates. By default, all predicates and facts only hold for the initial step of a variable. Eg
fact "init" {
no Offline
no connected_to
}
This fact says that in the initial step, there are no offline servers and no connection between clients and servers. There are no constraints, however, on future steps. To place constraints on future steps, put predicates inside a temporal operator, like always
or eventually
.
pred spec {
always no Offline
eventually some connected_to
}
run {spec}
always no Offline
means thatno Offline
is true now, and in all future steps.eventually some connected_to
means thatsome connected_to
is true in at least one step, now or in the future.
Temporal operators can be combined: eventually always some Offline
means that there’s a step where, from that step forward, there is some Offline server.
To model a “change”, we relate the values of a variable between two steps. If connected_to
is a var
field, then connected_to'
is the value of connected_to
in the next step.
pred connect[c: Client, s: Server] {
c -> s not in connected_to
connected_to' = connected_to ++ c -> s
}
In this example, connect
is true or false in every step. In steps where it is true, the client is not connected to the server and in the next step, it is connected to the server. This represents the state of the system changing.
'
is also called the prime operator. Combining primed predicates with temporal operators gives us a simple way to model system dynamics.
pred spec {
-- all servers always online
always no Offline
-- initially no connections
no connected_to
-- every step, a client connects to a new server
always some c: Client, s: Server {
c.connect[s]
}
}
run {spec}
List of Operators¶
Alloy operators include both future and past operators. Operators are true and false for a specific step.
always eventually once after after | before always | historically eventually | once until | since releases | triggered
Operator
Meaning
always P
P is true and true in all future steps
eventually P
P is true or true in at least one future step
after P
P is true in the next step
Shorthand for P && after Q
Q releases P
P is true until Q is true, then P may become false
P until Q
Equivalent to (Q releases P) and eventually Q
(P'
is special: instead of being true or false, it’s simply the value of the P in the next step.)
There are also past operators corresponding to each future operator. once P
is the past-version of eventually P
: P is true or true in at least one previous step.
Future Operator
Past Version
always
historically
eventually
after
before
triggered
releases
since
until
Recommend
-
283
This site can’t be reached www.growthmetrics.io refused to connect. ...
-
51
I'm trying to learn how to use and leverage the Alloy model checker in my day job and side projects but there doesn't seem to be much material in the way of basic examples for begin...
-
2
What You Need To Know About Gear Alloy Wheels Owning a vehicle come...
-
2
it's about Time • Hillel Wayne Skip to Content Alloy is a powerful formal specification language, but it’s historically been weak at modeling concurrency.
-
7
Learning DNS by modeling it with ALloy Alloy is a great tool to use for learning an unfamiliar domain by incrementally modeling it. I've never really grokked how the DNS system works,...
-
13
While custom keyboards are growing in popularity, many brands are raising the bar on pre-built options like the HyperX Alloy Origins 65. We went hands-on with the smaller
-
9
Aluminum alloy sheet price xuan posted @ 2022年6月10日 13:56 in 未分类 with tags
-
7
Marine aluminum alloy 5083 plate xuan posted @ 2022年6月13日 11:03 in 未分类 with tags
-
6
TechRadar Verdict For those looking for a portable gaming keyboard, the HyperX Alloy Origins 65 is a good place to start. It features colored backlighting, a fast response time, and the tactile feedback...
-
5
Home Technology NewsFirst 3D-Printed High-Performance Nanostructured Alloy That’s Both Ultrastrong...
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK