alloytools/alloytools.github.io

Website for Alloytools

alloytools.github.io's Issues

cup file link broken

The link to the cup file on this page is broken: http://alloytools.org/documentation.html

Ensure liveliness of links on Alloy's public website

Hello!
Multiple pages(citations, applications, etc.) have issues with the links. The issues vary from the content exists but the links need updating to contents no longer there, to domains no longer valid.
I will be submitting a pull request with fixes so per the guidelines this is the issue/branch I will be referencing.
Thanks for all the hard work!

"will be held [...] 2018" in community.md

"The Workshop on the Future of Alloy will be held in Cambridge, MA on April 30 & May, 2018." in community.md

Mistaken lexical grammar for 'greater than or equal to' token

In the reference manual (http://alloytools.org/spec.html), under the heading "Precedence and Associativity" is a list of "comparison operators", which is written as: "in, =, <, >, =, =<, =>", but the last of these is wrong, as I believe that => is only used for implication in Alloy, and it should be written as >= instead in this list.

The same problem appears in the reference manual under the heading "Boolean Expressions", which has the production:

compareOp ::= in | = | < | > | =< | =>

again I believe that => should be >= in this case, as just below this the manual says:

The constraint i >= j is true when i is greater than or equal to j.

The “less than or equal to” operator is written unconventionally with the equals symbol first so that it does not have the appearance of an arrow, which might be confused with a logical implication. For all these operators, the sum function is applied implicitly to their arguments, so that if a non-scalar set of integers is presented, the comparison acts on the sum of its elements.

Needs more recent versions on the downloads page?

I had to struggle a while with version 4.2 while it turns out there's a 5.1

Documentation issues regarding sequence operations and preconditions

There are some documentation errors for sequences (seq keyword), found at the following page:
http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html

Preconditions for sequence operations are stated in the documentation, but the meaning of a precondition in terms of model finding is not consistent. A formula which contains a seq operator with a false precondition is sometimes unsatisfiable, sometimes satisfiable.

Ideally, Alloy should not return a model where the precondition is false (ie, a predicate applied to a seq operator whose precondition is false should be valued as false also). However, this is certainly an issue to discuss individually.

For now, the documentation should be updated to reflect the current behavior.

Here is a list of preconditioned operators with their behaviour and an Alloy model test_seq_1.txt to illustrate them.

s.setAt [i, x]
Precondition: 0 <= i < #s
It should be : 0 <= i <= #s
Unsatisfiable if precondition not satisfied

s.insert [i, x]
Precondition: 0 <= i <= #s
Unsatisfiable if precondition not satisfied

s.delete [i]
Precondition: 0 <= i < #s
Unsatisfiable if i < 0
Satisfiable if i >= #s, returns the input sequence
Precondition should be : i >= 0

s.subseq [from, to]
Precondition: 0 <= from <= to < #s
Satisfiable if precondition is false, returns the empty sequence
Should not state a precondition

Pull request to follow.

Document new features in Alloy 6 as syntactic sugars

To help people make the transition from older versions of Alloy, such as in the book, and Alloy 6, it would be helpful to explain how one would desugar the new features into the older syntax without the new features. For example, I suspect that uses of var can be desugared into adding a time column and making other localized changes. An alternative would be to point people to where examples of the new features are and explain how those examples would be (or are already) written in the older syntax.

Browsers give HTTPS certificate warning for https://alloytools.org/

Chrome
NET::ERR_CERT_COMMON_NAME_INVALID

Firefox
Firefox does not trust this site because it uses a certificate that is not valid for www.alloytools.org. The certificate is only valid for the following names: www.github.com, *.github.io, *.githubusercontent.com, *.github.com, github.com, github.io, githubusercontent.com

Error code: SSL_ERROR_BAD_CERT_DOMAIN

Alloy6 image links broken

The "alloy 6" above the Mutable header should be an image.