Adding partial instance

[pkriens]

Is there a description of the syntax change? Was this change agreed upon with Daniel?

A bit concerned with all the whitespace changes. The way the Eclipse project is setup should make formatting automatically, was this edited in another editor?

[pkriens]

I am running this branch and find that an existing model and the results are scarily different. This is the original model on the current master branch:

Executing "Run run$1 for 12"
   Sig this/IP scope <= 12
   Sig this/Subnet scope <= 12
   Sig this/Node scope <= 12
   Sig this/Router scope <= 12
   Sig this/PC scope <= 12
   Sig this/IP in [[IP$0], [IP$1], [IP$2], [IP$3], [IP$4], [IP$5], [IP$6], [IP$7], [IP$8], [IP$9], [IP$10], [IP$11]]
   Sig this/Subnet in [[Subnet$0], [Subnet$1], [Subnet$2], [Subnet$3], [Subnet$4], [Subnet$5], [Subnet$6], [Subnet$7], [Subnet$8], [Subnet$9], [Subnet$10], [Subnet$11]]
   Sig this/Node in [[Node$0], [Node$1], [Node$2], [Node$3], [Node$4], [Node$5], [Node$6], [Node$7], [Node$8], [Node$9], [Node$10], [Node$11]]
   Sig this/Router in [[Node$0], [Node$1], [Node$2], [Node$3], [Node$4], [Node$5], [Node$6], [Node$7], [Node$8], [Node$9], [Node$10], [Node$11]]
   Sig this/PC in [[Node$0], [Node$1], [Node$2], [Node$3], [Node$4], [Node$5], [Node$6], [Node$7], [Node$8], [Node$9], [Node$10], [Node$11]]
   Generating facts...
   Simplifying the bounds...
   Solver=minisatprover(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   64870 vars. 2064 primary vars. 106945 clauses. 314ms.
   . found. . is consistent. 44ms.

The following is the identical model on this branch:

Executing "Run run$1 for 12"
   Sig this/IP scope <= [IP$0, IP$1, IP$2]
   Sig this/IP scope <= []
   Sig this/IP scope <= 3
   Sig this/Subnet scope <= [Subnet$0, Subnet$1, Subnet$2]
   Sig this/Subnet scope <= []
   Sig this/Subnet scope <= 3
   Sig this/Router scope <= [Router$0, Router$1, Router$2]
   Sig this/Router scope <= []
   Sig this/Router scope <= 3
   Sig this/PC scope <= [PC$0, PC$1, PC$2]
   Sig this/PC scope <= []
   Sig this/PC scope <= 3
   Sig this/Node scope <= []
   Sig this/Node scope <= [Router$0, Router$1, Router$2, PC$0, PC$1, PC$2]
   Sig this/Node scope <= 6
   Sig this/IP in [[IP$0], [IP$1], [IP$2]]
   Sig this/Subnet in [[Subnet$0], [Subnet$1], [Subnet$2]]
   Sig this/Node in [[Router$0], [Router$1], [Router$2], [PC$0], [PC$1], [PC$2]]
   Sig this/Router in [[Router$0], [Router$1], [Router$2]]
   Sig this/PC in [[PC$0], [PC$1], [PC$2]]
   Generating facts...
   Simplifying the bounds...
   Solver=minisatprover(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   1249 vars. 66 primary vars. 1862 clauses. 5ms.
   No instance found. . may be inconsistent. 1ms.
   . contains 1 top-level formulas. 3ms.

The model is:

sig IP {}

some sig Subnet {
    range   : some IP
}

abstract sig Node {
    ips     : some IP
}

sig Router extends Node {
    subnets : IP -> lone Subnet
} {
    ips = subnets.Subnet
    all subnet : Subnet {
        lone subnets.subnet
        subnets.subnet in subnet.range
    }
}

sig PC extends Node {} {
    one ips
}

let routes = { disj s1, s2 : Subnet | some r : Router | s1+s2 in r.subnets[IP] }
let subnet[ip] = range.ip
let route[a,b] = subnet[a]->subnet[b] in ^ routes 

fact NoOverlappingRanges        { all ip : IP |  one range.ip }
fact DHCP                   { all disj a, b : Node | no (a.ips & b.ips) }
fact Reachable              { all disj a, b : IP | route[a,b] }

run {
    # PC = 4
    # Subnet = 3
    # Router = 1
} for 12

[pkriens]

I initiated a discussion on the AlloyTools board because this PR causes a change in the syntax of Alloy.

There Daniel indicated that he want to see different proposals to this problem. I distributed the paper this change was based on and someone else submitted a proposal for partial instances on a model that did not require changes to the syntax by recognizing them based on some special patterns.

How are you planning to continue?

[aleksandarmilicevic]

The CompParser, Lexer, etc. file were deleted. This makes it extremely inconvenient to edit the project in Eclipse. We had decided I think that these files were stored in generated form to not force everybody to do a very inconvenient gradle build all the time. Since syntax changes are extremely rare this is is a small price for such a convenience.

Auto-generated files should not be version-controlled. You don't have to use gradle all the time; you can use it once to generate those files, and from then on you can use Eclipse or whatever other IDE you want.

[pkriens]

@aleksandarmilicevic I recall we had a discussion about this? I thought you accepted this because it is so inconvenient to always have to run gradle. Since syntax changes are very rare you it is easy to get out of sync and get weird errors if you don't put them under source control. Surprised, didn't we have this discussion?

[dnjackson]

Thanks for all your good work on this, Vajih!

This is actually the first proposal for a major change to Alloy, so we've had to figure out our process. See below for what we have in mind.

Our current concern is that it seems that are still regressions in which your version produces different results for existing models.

--Daniel

Process for Contributions to Alloy Codebase or Language

We welcome contributions to the Alloy toolkit and proposed language changes. Here is the process we are currently using for incorporating such contributions; post a message to the Alloy Google Forum to suggest an improvement.

1. If the contribution is a bug fix or improvement in performance that does not require a change to the documentation, you can just submit a pull request in the Alloy repo which will be considered by the Alloy maintainers. Please make sure to include test cases to ensure there are no regressions, and documentation explaining what you changed and why.

2. If the contribution is a major new piece of functionality, especially if it involves changes or extensions to the Alloy language:

— Submit a pull request that includes test cases and documentation explaining the contribution. In the case of a change that affects users, you should include a short FAQ and brief documentation to be included in the language description (eg, grammar rules, semantics). You should also include executables and sample models so other members of the community can experiment with your new version. Contact Peter Kriens if you need help building the executables. Most importantly, you should include a document that gives a brief outline of the proposal explaining it to the members of the Alloy forum. This document can be in any format you choose; it could be a short slide deck, or a technical memo.

— The Alloy maintainers will announce the proposal to the forum, and after some period of discussion, the Alloy Board will meet to consider the proposal. If accepted, the proposed changes will be included in the official release. If not, you may be asked to alter your proposal. Note also that in cases where your proposal involves a feature that others have also proposed, the Board may want to group several proposals together, which may result in things taking a bit longer.

[vmontagh]

Thanks for reviewing and explaining the contribution process. I have seen others interest in the work and decided to submit this PR showing the idea and implementation. What proposed here was mostly done years ago for research experiments ran by colleagues and myself. I also think releasing a stable implementation of this feature needs more effort. Regardless of the mentioned regressions, I believe the PR offers enough to clarify the new syntax and a way of realization. I'll be glad to improve the implementation and mitigate regressions if there is a consensus on a future for this PR.

[pkriens]

This is outdated. If still interested in supoorting this please update this for Alloy 6