hwayne / alloydocs Goto Github PK
View Code? Open in Web Editor NEWProposed documentation for alloytools.org
License: MIT License
Proposed documentation for alloytools.org
License: MIT License
Provide the example of #univ
in the evaluator
Welcome to the Alloy Documentation!¶
— strange title
Each model will have some number of each signature, called atoms. Take the following spec:
The following would be a valid model:
— uses model in two different ways
We don’t just care that there are people and accounts, we care which people have which accounts.
— Odd that this introduces an example that doesn’t relate to the example that follows in the code
Standard convention is to prefix every relation with a comma.
— your convention maybe :-)
— commas motivated in part by ability to write inline: sig A {b: C, c: C}
Alloy can generate models where a relation points to the same atom.
— not clear what this means
Each relation has a multiplicity, which represents how many atoms it can include. If you do not include a multiplicity, it’s assumed to be one.
— not true for relation with arity > 2
, edge: set Node - this
— more natural to call this field “adjacents” or even “edges”, or do you mean it to represent a hyperedge?
Using the dot operator, if access = P -> C -> D, then P.access = C -> D and access.D = P -> C.
— introducing this for multi relations. why not for relations?
As an aide, use the following table:
— aid?
— why the “used” terminology? I’m not sure what it means.
If you make a signature abstract, then all instances of the signature will be extensions
— what does instances mean here?
Then the b relation can include A -> C, but c cannot include A -> B.
— not sure what “can include” means. i think there’s an instance in which c does include A->B.
In sets and relations:
All elements of a set must have the same arity, but can otherwise freely mix types of elements.
— Seems misleading to me: elements cannot be sets or relations.
Adding a signature automatically defines the set of all atoms in that signature. Given
— Perhaps confusing? signature name also the name of a set?
univ -> univ is the set of all possible relations in your model.
— the largest relation?
one sig U1, U2 extends User {}
— not sure it’s clear how the relation U1 relates to the atom U1
Return every element that elements in Set map to, via rel. This also works for individual atoms.
— typo
We can use the dot operator with two relations. It returns the inner product of the two relations.
— Note that dot isn’t overloaded: it’s the same operator in every case. I think it’s important to point this out.
This is mostly useful for directly manipulating relations. For example, given a set S, we can map every element to itself by doing S <: iden.
— also useful for disambiguating field names
A bar expression is one of the form:
— but let also has a bar?
— other quantifiers eventually go here?
— looks like you have quants later, so this is a remnant?
one and lone behave unintuitively when used in multiple quantifiers.
— actually, i think they behave intuitively — as your explanation following this suggests. the problem is that the shorthand rule (that you can expand Q x, y | into Q x | Q y) doesn’t hold.
The following truth table will satisfy clause (2) but not (1):
— maybe better to use S1 and S2 rather than A, B?
The parameters of a function (or predicate) can shadow a global value. In this case, you can retrieve the original global value by using @Val.
— I have no recollection of this!
Commands
— useful to be able to attach labels to commands
foo: check…
so they appear in menu
Tooling
The analyzer converts the model into a SAT expression to solve. S
— SAT instance? SAT formula?
Techniques
Then the boolean can be tested with a in PremiumAccount. This method has a number of advantages:
— also can write things like
PremiumAccount.owner in Member
rather than
all a: Account | a.premium = true implies a.owner in Member
If subtyping is insufficient, you can also use the boolean module. This is generlaly not recommended.
— typo
Dynamic Models
— would be nice to include events, which visualize better than predicates
https://alloy.readthedocs.io/en/latest/language/signatures.html#abstract
I believe the example should be :
abstract sig Machine {}
sig Broken in Machine {}
sig Server extends Machine {}
sig Client extends Machine {}
To show that you can have Clients or Servers possibly in Broken but no Machines, or Broken Machines.
I’d like to contribute to this documentation, but I can’t find any licensing information in the repository. Am I missing something?
Thank you.
It's been almost a year, c'mon man
The link to "here" in the readme is broken (points to https://github.com/hwayne/alloydocs/blob/master which triggers a page not found). Is it supposed to point to https://github.com/hwayne/alloydocs/tree/master
maybe?
I noticed there are no links to https://alloy.readthedocs.io/en/latest/ when browsing the github project, I believe the description of the project is the right place to store that information.
Version 5.0 added support for Markdown syntax.
Even just importing the linked docs verbatim would be useful. Heck, I can submit that as a PR if you're supportive.
Love the new docs. I made some notes as I was going through:
r: some A states that there is at least one A in the relation.
But the image shows one
multiplicity. Each book has one author.
univ.rel is the domain of rel
This is range. Domain is rel.univ
.
We can write both ~^edge and ~^edge.
These two are the same. Perhaps one of them is supposed to be ^~edge
?
*edge = ^edge + iden
Not strictly true, I hope. I am curious, though, does *(A->B)
contain B->B
?
rel1 ++ rel2 = rel1 - (univ.rel2 <: rel2) + rel2
I believe this should be (rel2.univ <: rel1)
. Also "shared relationships" is not clearly defined.
=> can also be used as a constraint.
This confused me. I believe the =>
operator hasn't been introduced yet at this point of a linear reading. And the link on "constraint" wasn't to anything that would define that term.
Bar expressions
It is unclear if the newline after the |
is required.
To say that A is not a subset of B, you can write A !in B, A not in B, !(A in B), etc.
It was surprising to find !in
given such little attention, since it is definitely a thing in other languages.
Relational Quantifiers
It is surprising that you can use some
but not no
. Also why isn't all
supported when you can just write it with chained quantifiers?
all e: rel | P[e]
≡ all x: rel.univ | all y: x.rel | P[x->y]
I like to use a vertical monitor off to the side for reading documentation as I work. On the Alloy page, the left index bar takes up a large amount of screen space:
It would be nice if the index bar could be collapsed, similar to in the Python docs: https://python.readthedocs.io/en/latest/index.html
The wording of
https://github.com/hwayne/alloydocs/blame/master/language/signatures.rst#L472
If you make a signature ``abstract``, then all instances of the
signature will be extensions, and there will be no signatures that are
still the base.
confuses me - what is the base? "still the base" signature? maybe "only the base signature"?
And is "base" defined somewhere? Or does this mean supertype of a suptype?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.