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.
573
questions
0
votes
0
answers
18
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
42
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
39
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| ...
0
votes
0
answers
26
views
Why is table View blank in Alloy
I am trying to modularise my Alloy model by splitting and grouping parts into some other Alloy files. But, when I execute the Alloy Analyser, the Table View, which I find the most useful view, is ...
0
votes
0
answers
22
views
Parametric modules sending ordering/list parameter
I am trying to pass an "ordering/list" parameter to the parametric module as the following. Is it possible to do such thing as in the following example?
module combined [VendorState, vs]
...
1
vote
1
answer
55
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
31
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
0
answers
149
views
Modelling git properties or restrictions on Alloy
So I need to specify the properties of the git object model in Alloy,
where the object model is defined as follows:
sig Hash {}
abstract sig Object {
hash : one Hash
}
sig Blob extends Object {}
...
0
votes
1
answer
74
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
298
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
58
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
23
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
127
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
86
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
54
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
76
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
129
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
126
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
43
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
24
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
29
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
60
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
48
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 | ...
0
votes
1
answer
82
views
Alloy Analyzer: Quantifiers and Set Products
I have encountered the following issue in Alloy. Consider the toy code which tries to capture even labeled entities (V1 is for State and V2 is for ProductStateSet):
enum State {s1, s2, s3, s4, s5, s6}...
0
votes
1
answer
42
views
Why does the Alloy API not use the default scope for one signature if the scope for a different signature is specified?
I am currently attempting to run the following Alloy model on the Alloy Analyzer 5.1.0:
sig parent {}
sig var {}
pred testPred{}
run testPred for 3 parent
However, attempting to run this model ...
0
votes
1
answer
24
views
Declaring a field as `f: elems[g] -> one h` is producing a name-not-found error. What am I missing?
In a model I am writing, I would like to say that a reading of a manuscript identifies a sequence of tokens in the manuscript and maps them to types; the mapping should be defined for all tokens in ...
0
votes
0
answers
31
views
Alloy Show Functions in Submodule
I have a module test.als
module test
sig Sig1 {}
fun f:Sig1->Sig1 {iden}
run {#Sig1 = 1} for 1
and a submodule test2.als
module test2
open test
run{#Sig1=1}
But if I execute this and look at ...
1
vote
2
answers
55
views
Comparing a concrete execution trace with an Alloy Model
I'm using Alloy to model a system. I would like to check the implemented system matches the Alloy model by comparing log traces from a concrete execution of the actual system with the model.
The way I ...
1
vote
1
answer
51
views
Alloy - Irreflexivity
I just started using Alloy. I have a question about the following minimal example:
module test
abstract sig MySig {
my_rel : set MySig
}
//fact my_rel_irrefl {no iden & my_rel } // this ...
0
votes
3
answers
77
views
Predicate not consistent
I have to realize an application which permits to reserve a seat in a store. There are no sintax error, but I don't understand why terminal reply me "predicate not consistent". Can u help ...
0
votes
1
answer
50
views
Count with Alloy under a specific condition
I need to count how many ticket have the same time and, then, to compare this number with the maximum permitted seats at a specific hour, but I'am experiencing some problems in this task. How I can ...
1
vote
2
answers
68
views
Getting subsets of signatures in Alloy
I was wondering if there is a way to extract a subset of a set in a given signature in Alloy.
The extracted set will then be used in the definition of some facts of the model.
Assume the following ...
0
votes
1
answer
38
views
Alloy API: Decompile into .als
BLUF: Can I export a .als file corresponding to a model I have created with the Alloy API?
Example: I have a module that I read in using edu.mit.csail.sdg.alloy4compiler.parser.CompUtil. I then add ...
0
votes
2
answers
43
views
Is it possible to declare alias fields in Alloy?
In my current model, I am finding it helpful to define alias fields. These are fields that are really just expressed as an expression of an existing field. I recently discovered the = syntax for ...
0
votes
0
answers
31
views
Why does Alloy-as-Markdown search for ModuleNameg.md rather than ModuleName.md given open ModuleName?
I have a .md file containing this fragment:
---
title: behaviour of vehicle locking system
layout: default
description: concrete example drawn from 2019 Ford Transit users handbook
---
```alloy
module ...
0
votes
1
answer
51
views
How are inital states established in dynamic models under Electrum 2?
I cribbed from the hotel door lock example and came up with this MWE for vehicle doors.
enum LockState {Locked, Unlocked}
sig Door {
var state: LockState
}
sig Vehicle {
doors : disj set ...
0
votes
1
answer
76
views
How can I run the Alloy model checker API in Eclipse?
I am having trouble importing Alloy libraries to use the API in Eclipse. This is the code I am trying to run: http://alloytools.org/documentation/code/ExampleUsingTheAPI.java.html
The problem is that ...
0
votes
1
answer
102
views
JAVA_HOME not working to run gradlew build ( for Alloy Model Checker)
I am installing Alloy Model Checker (https://github.com/AlloyTools/org.alloytools.alloy).
I cannot run gradlew build.
$ C:\Alloy\org.alloytools.alloy>gradlew build
ERROR: JAVA_HOME is set to an ...
0
votes
1
answer
69
views
Violate fact in alloy
I'm creating bell lapadula and this is my code.
abstract sig classificaion{}
one sig classified extends classification{}
one sig unclassified extends classification{}
sig user{ level: one ...
0
votes
2
answers
80
views
Exception in thread "main" Syntax error: This module cannot be found. Java Alloy program not compiling
I have written a Java program that will execute an Alloy (.als) file. When I am using the commandline the program works perfectly but when I try to run it using NetBeans, this error is shown:
...
1
vote
2
answers
66
views
How to derive the `one` multiplicity constraint using the Alloy Kernel language?
I was reading Appendix C: Kernel Semantics of the Software Abstraction book (by Daniel Jackson, second edition, very nice read btw!) and found myself a bit stuck in understanding how to derive the one ...
0
votes
0
answers
30
views
Is there a way to assign a signature the abstract attribute after it has been instantiated?
I would like to do something similar to the following:
PrimSig sig = new PrimSig(sigName,parent);
sig.isAbstract = True
but obviously the preceding example is not possible since the isAbstract ...
0
votes
2
answers
73
views
Alloy : Restrict values of a String field
Let the following simple Alloy code :
sig somme{
f : one Ax1,
g: one Ax2,
}
let Ax1= String
let Ax2= "Spain" + "Italy"
I want to restrict the values of the field f to "Italy" so I write a predicat :
...
0
votes
2
answers
77
views
Alloy:How to understand the counterexample in the Alloy demo?
I write a strange Alloy demo about "assert" out of curiosity.
Assume there is a "Program", the "Program" has 2 "Varieties", and each "Variety" has a "Value" from "Data" set.
Then I also set a "fact"...
0
votes
0
answers
40
views
How To Use CompUtil To Parse With Plugin
When using the Alloy API to perform parsing on the following string:
Module mod = CompUtil.parseEverything_fromString("run {} for 5")
I receive the following error:
Fatal error:
Parser Exception
...
0
votes
1
answer
33
views
Alloy:How to define the relations between two modules without the module dependency error?
Previously, I defined two simple signatures so that I can know which car does this wheel belong to.
sig Car{
wheels: some Wheel
}
sig Wheel{
BelongCar:one Car,
}{
BelongCar=this.~@...
1
vote
2
answers
59
views
Alloy pred declaration: is there a difference between square brackets and parentheses?
The question probably has a yes/no answer. Consider the snippet:
sig A { my : lone B }
sig B { }
pred single1 [x:A]{ // defined using []
#x.my = 0
}
pred single2 (x:A){ // defined using ()
#...
0
votes
1
answer
111
views
Dynamic modeling with Alloy
I'm evaluating a co-worker's pitch using Alloy to model the problem and gain insight into additional questions/constraints that are required to meet the specification.
I believe that Alloy is the ...
0
votes
0
answers
38
views
Lock and Key Problem Solution using Alloy
I am new to alloy and was trying to pose the following puzzle given to me by a friend in terms of Alloy constraints
682 one digit is right and in its right place taken
614 one digit is right but in ...