Questions tagged [alloy]
Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the resulting structures.
598
questions
0
votes
0
answers
10
views
Should the book example be refined to avoid inconsistent results
When existing Alloy models of the book example are used in Alloy 6.1,
the evaluation results give contr-intuitive representation of add operation:
In the book instance Book$0 Name$1 is related to ...
-1
votes
1
answer
49
views
How to integrate Regex into Alloy Analyzer?
I am currently modeling a container orchestrator using Alloy. It turns out that many of the facts I need to write involve regular expressions (regex). Since regex is not supported by default in Alloy, ...
0
votes
1
answer
30
views
Alloy6 allowing invalid state transitions
This is my spec, it tries to model a Sale with multiple Orders:
abstract sig Sale {
var status: one Status,
orders: some Order,
amount: Int
}
enum Status { Pending, Ok, Err }
sig ...
1
vote
1
answer
27
views
From predicate calculus style to relation calculus style in Alloy
I have two Alloy facts:
fact A5 {
all a, b : Filler, s, t : Slot |
(b in s.slot_of and s in a.fills and a in t.slot_of) implies b in t.slot_of
}
fact A6 {
all a, b : Filler, s, t : Slot | ((b ...
0
votes
1
answer
29
views
Alloy analyser - only natural numbers - no integer set
Is there a way to declare the natural numbers as in Int in Alloy?
Currently I have util/integer and if I run run 6 Int I get:
integers={-32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, ...
0
votes
1
answer
33
views
Pass parameter to predicate with Alloy Java API
How can I create an instance of atom with Alloy API? My goal is create an instance from java and pass it as a parameter to predicate alloy model.
The issue is:
Field "field (this/File <: name)&...
1
vote
1
answer
59
views
Implication vs. Disjunction operators
I must have a misunderstanding somewhere. Here is a specification of everyone's favorite bank account/transfer system:
sig User {
var balance: one Int
}
var one abstract sig Message {}
var lone ...
0
votes
1
answer
51
views
Alloy: unexpected instance, difference between Sig'=Sig & Sig.field' = Sig.field
I am trying to model the following properties:
Given a computation rule, and an Observable (~asset) we may raise an alert for this pair of (rule, observable).
User can disable some rules, and we won'...
0
votes
1
answer
26
views
Nested maps in Alloy
I'm trying to model nested maps in Alloy (e.g. {a: {b: 3}}) where mapping such as {a: {a: 3}} with the same key repeated are invalid. I tried to do this with the final fact listed below, but I'm ...
0
votes
1
answer
34
views
No Instance Found on integer declaration greater than 7
I'm trying to model a problem that about some girls on the pool. There are some premises that must be followed.
Maiô: amarelo, azul, branco, verde
Nome: Ana, Bruna, Raquel, Vivian
Idade: 8, 9, 10, 11
...
1
vote
3
answers
76
views
Alloy book example is wrong?
Reading Software Abstractions by Daniel Jackson. Tried creating a simple model, realized it's not working the way I intend. Came back to the most basic models in the book which are 1:1 to my own, and ...
0
votes
1
answer
694
views
Problem using JPype on Mac OS X: I try to start the JVM but I get a DLL not found, but it is there
My Python code is:
import jpype
jvm_path = "/Library/Java/JavaVirtualMachines/microsoft-11.jdk/Contents/Home/lib/jli/libjli.dylib"
jpype.startJVM(
jvm_path,
classpath=['~/org....
0
votes
1
answer
48
views
Why do Alloy Analyzer generated the same solution multiple times?
Why do Alloy Analyzer generates the same solution multiple times?
(https://alloytools.org)
Example.
As a dummy example, consider the next Alloy model. If you run code in the Alloy Analyzer it ...
0
votes
1
answer
37
views
Define elevator floors (symmetry, ordering) in Alloy
I'm trying to specify an ordered set of floors in Alloy 6, so that I can later simulate an elevator visiting those floors.
Ultimately, I want to generate a graph that looks like the image below:
...
0
votes
1
answer
24
views
Modeling a presentation with ordered slides
I’m trying to model a presentation with ordered slides, with every slide appearing in exactly one presentation.
sig Presentation {
// At most #Int arrows, exactly #Slide arrows, each Int used at ...
1
vote
1
answer
70
views
How to specify "global" frame condition in Alloy6?
I am trying to model temporal process using for reference Formal Software Design with Alloy 6 - Protocol design chapter. I would like to know how to make frame conditions in predicates less verbose.
...
0
votes
1
answer
38
views
No more satisfying instances
No examples generated for my alloy model with the error message: 'No more satisfying instances' (see image attached)
I have created the following small model in Alloy:
sig System
{
subSystem : ...
0
votes
1
answer
41
views
how to set constraints on a ternary relation
I have this model
sig Factor {}
sig Rule { rule : some Factor }
sig RuleSet { rules : some Rule }
sig EventRuleProperty {}
sig Event {
rulesets : some RuleSet,
rule_properties : ...
0
votes
1
answer
62
views
Alloy dynamic modelling with predicates
I am trying to model in alloy a system where the users can make comments on forum threads. I want to describe with a predicate a situation where a new comment is added to a forum thread.
This is what ...
0
votes
1
answer
42
views
Alloy: different instances for integer
I'm new to alloy and i'm doing a little project. In the project i have some instances with different attributes that, with magic layout, i can put in the instance when showing the model. Is there a ...
0
votes
1
answer
69
views
Creating a List Specification in Alloy Language
I'm working on defining a List in Alloy but I'm stuck.
This is what I have so far (it acts like a LinkedList):
module List
// The List signature
lone sig List { rootElement: lone Element }
// A ...
0
votes
1
answer
78
views
Conversion to Alloy 6
I'm running Alloy 6 (6.1.0) for the first time. I've updated my syntax and am getting no error messages. But checking assertions (that were valid in Alloy 5) I am fairly often getting:
0 vars. 0 ...
0
votes
1
answer
65
views
How To Prevent Circular Relationships In Model?
I'm working with Alloy 6 and I'm attempting to model a system to create packages for various package managers. For example the system might create a Rebar3 (Package) for maybe ChocolateyNuget and ...
0
votes
1
answer
44
views
Why does alloy model with but 1 set A return instance of more than 1 A
I am sorry for the title, I tried hard to make it as understandable as possible but I know I failed.
Here is the simple model:
sig ETHBusStation {
next: set ETHBusStation
}
one sig Polyterrasse, ...
0
votes
1
answer
40
views
Why does Alloy not find a counter-example for a simple tree structure?
Here is a minimized Alloy model I tested with Alloy 6.1.0 on macOS:
sig Root {}
sig NonRoot {
root : one Root,
parent : lone NonRoot
}
fact acyclic {
no i : NonRoot | i in i.^parent
}
fact ...
2
votes
1
answer
81
views
Why would prime (aka ') raise an error in the following: pred add (b, b': Book, n: Name, a: Addr) { b’.addr = b.addr + n -> a }?
I have Alloy 6.1.0 running on Windows 10
I have "Software Abstractions" text by Daniel Jackson and working through book.
I am at the examples in the "Whirlwind Tour" and section 2....
0
votes
1
answer
74
views
using electrod/nuXmv solver with Alloy on Windows?
I have nuXmv installed and added to my path on windows but have not seen instructions anywhere for adding it to the options->solvers menu on windows.
0
votes
2
answers
78
views
No Instance Found When Using "always"
I'm trying to visualise a spec for a Payment object where it moves from "queued" to "processing" to "complete". I have come up with the following:
enum State {Queued, ...
0
votes
1
answer
34
views
Predicate-Polymorphic Modules in Alloy?
In alloy you can make modules polymorphic on signatures by defining them as arguments in the module definition, e.g.:
module mymodule[sigA,sigB]
In my case, I also want to have predicates about these ...
0
votes
1
answer
43
views
Forcing InProgress state machines to always resolve
I am trying to model executions of concurrent AWS Lambda functions to look for bugs around timing. In my model, once a Lambda is triggered, it should always end up in either a Complete or Failed state....
0
votes
0
answers
46
views
Why does the Alloy API solution's ".next()" method keep returning the same solution? Can I force it to return the next unique solution?
Can anyone explain why the Alloy API solution's ".next()" might return the exact same solution ad infinitum? It doesn't always, but when it does, I get stuck in an infinite loop. Is there ...
0
votes
1
answer
106
views
Trying to solve Lady or the Tiger in Alloy
I've been trying to solve the logic puzzle Lady or the Tiger in Alloy but got stuck. Right now I'm trying to solve the 4th puzzle which is on the 2nd day.
It goes as following: There are a few rooms ...
0
votes
1
answer
56
views
Get greater number in a field? Alloy model checker
I want to return the greater number max(loc.x) in a field scope:
sig Locations{
x: set Int // all x locations visited
xgreater: one Int // greater location
}
fact{all loc:Locations| ...
1
vote
1
answer
87
views
Alloy assertion on implies command
I try to implement on Alloy the axiomatic system described in a paper on mereology: "Bennett, Having a Part Twice Over, 2013".
I implemented all the axioms, and I thought that if I ...
0
votes
1
answer
69
views
Alloy API throws a Null when executing alloy command
I have been using the Alloy API which can be written in Java. My goal is to compile Alloy model, display it visually, and narrow down the search for instances.
At this time, I need to command the ...
0
votes
1
answer
150
views
How do I see the returned value(s) of a function in Alloy?
I'm trying to understand how functions work in Alloy, and an important part of that is testing them. For example I've got this code:
open util/ordering[Time] // enforces total order on Time
sig ...
5
votes
2
answers
644
views
Solving predicate calculus problems with Z3 SMT
I'd like to use Z3 to solve problems that are most naturally expressed in terms of atoms (symbols), sets, predicates, and first order logic. For example (in pseudocode):
A = {a1, a2, a3, ...} # A is ...
0
votes
1
answer
107
views
How to know the number of models found by Alloy Analyzer?
Is there a way to know how many output models Alloy Analyzer finds?
I need to know how changing the alloy model changes the number of Alloy instances found.
Thanks!
0
votes
1
answer
31
views
Keep the same index in Alloy Analyzer?
I want to allocate a machines to operators. Each machine has a fix set of works (e.g., machine1 does work2 and work). Here a simple output example with 2 operators (operator1,operator0) and 3 machines ...
2
votes
2
answers
308
views
How to sum more than two numbers in Alloy Analyzer?
I am trying to sum all the numbers in a set in Alloy.
For instance, in the signature abc, I want the value to be the sum of a.value + b.value + c.value, which is 4+1+3=8.
However, if I use "+&...
1
vote
2
answers
185
views
Checking Sig Equality in Alloy
In the following Alloy model I want to check the equality of two instances of a sig with Bool field type:
module test
open util/boolean as bool
sig Info {
active: Bool
}
assert assertion {
...
0
votes
2
answers
76
views
Alloy specifications
I'm a beginner learning Alloy, I want to know what means this n.^address (maybe with an example)? because logically if we consider address as a set of pairs like (A0,A1), then how we can join n which ...
0
votes
1
answer
206
views
How Can I Specify All Members of a Set Are Unique in Alloy?
I have an alloy model. In the spirit of a small reproduction example, I've extracted the following:
sig SearchTerm {}
sig Document{
keyword: set SearchTerm
}
assert keywordsAreUniqueForDocument {...
1
vote
1
answer
295
views
What does it mean to "run" a function in Alloy?
My understanding is that functions in Alloy return a value. However, I noticed that you can run a function using a run command the same way you would run a predicate. What does running a function mean ...
2
votes
1
answer
306
views
What is the difference between assertions and unparameterized predicates in Alloy?
Is there a difference between an assertion and an unparameterized predicate in Alloy? You can use the "check" command on both unparameterized predicates and assertions to find a ...
0
votes
1
answer
58
views
What is the purpose of abstract signatures with no fields in Alloy?
I frequently see modelers using abstract signatures with no fields in their models. The abstract signatures usually have subsignature extensions but no fields. For instance, consider the following ...
0
votes
1
answer
45
views
In the tutorial part II, why can Alloy compose root with parent?
In the File System Lesson II of the Alloy Tutorial, the following model is described:
// A file system object in the file system
abstract sig FSObject { }
// File system objects must be either ...
0
votes
0
answers
54
views
How to create a "run" command from the Alloy API?
I'm trying to run a predicate, Test1, from inside the Alloy API. I create a command to run Test1 in my program like this:
Expr predExpr = funcWithName("Test1").call();
Expr factExpr = this....
1
vote
1
answer
86
views
Let declarations outside of blocks in Alloy
I recently came across some Alloy models that have "let" statements that do not pertain to any block in the model. The Alloy Analyzer parses these models just fine so I know this is valid ...
1
vote
1
answer
82
views
Remove predicate relations in Alloy
I'm learning how to use Alloy, and I've coded this:
module test/SlotsAndFillers
sig Slot { content: one Filler}
sig Filler { slots: set Slot}
fact AllSlotsAreOwned {
all s:Slot | some x:Filler | ...