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.

Filter by
Sorted by
Tagged with
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 ...
Eduard BABKIN's user avatar
-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, ...
bd36's user avatar
  • 1
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 ...
Pablo Fernandez's user avatar
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 ...
Lepticed's user avatar
  • 353
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, ...
Griselle Z's user avatar
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)&...
HKS's user avatar
  • 167
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 ...
Alexander Bakst's user avatar
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'...
dgan's user avatar
  • 1,379
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 ...
Michael Mior's user avatar
  • 28.2k
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 ...
George Victor's user avatar
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 ...
user avatar
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....
Rodrigo Stv's user avatar
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 ...
Griselle Z's user avatar
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: ...
Seanny123's user avatar
  • 8,886
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 ...
Marko Mušnjak's user avatar
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. ...
Matija Sirk's user avatar
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 : ...
Dirk-Jan Swagerman's user avatar
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 : ...
PeterJ's user avatar
  • 13
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 ...
Carlo Sgaravatti's user avatar
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 ...
Daniele00's user avatar
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 ...
Cyberboy1551's user avatar
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 ...
Pamela Zave's user avatar
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 ...
Onorio Catenacci's user avatar
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, ...
Olli's user avatar
  • 946
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 ...
typesanitizer's user avatar
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....
Asterion Daedalus's user avatar
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.
Juan Benavides's user avatar
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, ...
FormalizeMe's user avatar
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 ...
Goens's user avatar
  • 407
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....
gordonc's user avatar
  • 532
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 ...
J. Eanes's user avatar
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 ...
Myrqz's user avatar
  • 51
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| ...
Griselle Z's user avatar
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 ...
Lepticed's user avatar
  • 353
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 ...
p4mera's user avatar
  • 1
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 ...
chai_tea's user avatar
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 ...
SRobertJames's user avatar
  • 8,581
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!
Griselle Z's user avatar
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 ...
Griselle Z's user avatar
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 "+&...
Griselle Z's user avatar
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 { ...
Branky's user avatar
  • 373
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 ...
shabnamshmli's user avatar
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 {...
Onorio Catenacci's user avatar
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 ...
E. Eid's user avatar
  • 49
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 ...
E. Eid's user avatar
  • 49
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 ...
E. Eid's user avatar
  • 49
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 ...
geonnave's user avatar
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....
moonish's user avatar
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 ...
E. Eid's user avatar
  • 49
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 | ...
Lepticed's user avatar
  • 353

1
2 3 4 5
12