hwayne/alloydocs

Proposed documentation for alloytools.org

alloydocs's Issues

Some minor issues while reading through the new docs.

Love the new docs. I made some notes as I was going through:

https://alloy.readthedocs.io/en/latest/language/signatures.html

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.

https://alloy.readthedocs.io/en/latest/language/sets-and-relations.html

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.

https://alloy.readthedocs.io/en/latest/language/expressions-and-constraints.html

=> 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]

Explain limitations on arithmetic better

Provide the example of #univ in the evaluator

License

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.

"Here" link broken

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?

bunch of small comments

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

Document Markdown syntax

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.

signature abstract subtype is missing abstract in example

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.

Awkward/Unclear explanation of `abstract`

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?

Make multirelations signature table clearer

Consider adding the url of the doc to the github project description

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.

Update for Alloy 6

It's been almost a year, c'mon man

UI layout: enable collapsing index bar on left for improved use of screen space

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

Add events example to model dynamics