A4 module resolution paradox

[Nicolas F Rouquette]

Hi,

Alloy3 had a module search path variable similar to Java's classpath.
This went away in Alloy4 which makes user-defined A4 specifications
location-dependent
in contrast to A4's standard library and book examples which are
location-independent.

This asymmetric handling of module names in 'open' statements leads
to a rather strange paradox, e.g:

module foo   -- specification foo is in ./foo.als
open util/relation -- ./util/relation.als is optional
open util/table -- ./util/table.als is required
open bar/baz -- ./bar/baz.als is required

This paradox induces an unfortunate consequence: for a given Alloy4
application,
all of the location-dependent specifications  that the A4 compiler loads
must
be accessible as relative pathnames from the current directory.

In turn, this induces a lot of duplication of A4 specifications.
For example, the relative path util/table.als must be valid
in each directory where it's referenced as 'open util/table'.

In Alloy3, there is support for a module search path variable in
alloy.util.FileUtil
Why was this removed in Alloy4?

In Alloy4, there is a limited search path mechanism
to search for a module in the file system or in alloy4.jar.
See: edu.mit.csail.sdg.alloy4.Util.canon(String filename) and
edu.mit.csail.sdg.alloy4.Util.readEntireFile(boolean, String)

This is really a special case of a URL resolver for a fixed set of
URL resolution rules mapping the module filename into a file: URL
or a jar: URL. Could this be turned into a dynamic resolution mechanism
that would give us the same functionality as a user-defined search path
variable?

-- Nicolas.

[Felix Chang-2]

On Sat, 5 Apr 2008, Nicolas Rouquette wrote:

> Alloy3 had a module search path variable similar to Java's classpath.
> This went away in Alloy4 which makes user-defined A4 specifications
> location-dependent in contrast to A4's standard library and
> book examples which are location-independent.
>
> This asymmetric handling of module names in 'open'
> statements leads to a rather strange paradox, e.g:
>
> module foo   -- specification foo is in ./foo.als
> open util/relation -- ./util/relation.als is optional
> open util/table -- ./util/table.als is required
> open bar/baz -- ./bar/baz.als is required

Dear Nicolas:

Actually Alloy4's module inclusion mechanism is a bit more complicated.
It is explained in bullet #9 in the "New Syntax" section of Alloy4 Quickguide,
but let me elaborate it with a full example.

Suppose you have a "message.als" like this:

     module nicolas/project1/message
     open nicolas/project1/packet
     open nicolas/common/tcpip

1) The module line tells AlloyAnalyzer that message.als
must reside at <ROOT>/nicolas/project1/message.als
So if message.als is at /users/Nicolas/alloy/nicolas/project1/message.als,
then Alloy Analyzer will infer that <ROOT> is /users/Nicolas/alloy

2) "open nicolas/project1/packet" means
to load <ROOT>/nicolas/project1/packet.als
In this case that means /users/Nicolas/alloy/nicolas/project1/packet.als

3) "open nicolas/common/tcpip" means
to load <ROOT>/nicolas/common/tcpip.als
In this case that means /users/Nicolas/alloy/nicolas/common/tcpip.als

4) There are two additional rules:

4a) If the "module" line is omitted in a particular ALS file,
then we assume <ROOT> = the directory containing this ALS file.

4b) Alloy has a few useful libraries like "integer.als" and "ordering.als".
Back in Alloy3 days, these were called "util/integer" and "util/ordering".
So now, for compatibility reasons, when we see "open util/ordering",
and you don't actually have such a file,
then we assume you are referring to one of these util libraries.


> This paradox induces an unfortunate consequence...
> In turn, this induces a lot of duplication of A4 specifications.
> For example, the relative path util/table.als must be valid in
> each directory where it's referenced as 'open util/table'.

Your claim that "The relative path ... must be valid in each ..." is incorrect.
You just have to define the "module" line correctly.

Suppose /home/project1/main.als says:
module project1/main
open util/table
...

Suppose /home/project1/input/inputDriver.als says
module project1/input/inputDriver
open util/table
...

Suppose /home/util/supertable.als says
module util/supertable
open util/table
...

Suppose /home/util/table.als says
module util/table
...

Then main.als and inputDriver.als and supertable.als will ALL correctly
import table.als, even though they are all at different locations
in the file system.

So what you fear does not happen: modules that import table.als
do not need to all be at the same level in the file system,
nor do you need to duplicate "table.als" multiple times in your file system.


>
> In Alloy3, there is support for a module search path variable in
> alloy.util.FileUtil. Why was this removed in Alloy4?
>

I felt that the new automatic inferrence (when used correctly)
should eliminate the need to fuzz with custom-defined search path variables.


>
> In Alloy4, there is a limited search path mechanism
> to search for a module in the file system or in alloy4.jar.
>

This "search mechanism" is solely used to support the historical
util/ordering util/integer util/relation library files...
It is not intended and cannot currently be used by users
to "resurrect" the Alloy3 search path variable mechanism.

Sincerely,
Felix Chang
Alloy4 Developer

[Nicolas F Rouquette]

Hi Felix,

I hadn't realized that the A4 module mechanism had this much
flexibility. It's indeed well thought out.

My problem stems from difficulties in providing access to A4
specifications as resources in Eclipse plugins.

Suppose we have:

org.example.alloy.table.plugin exposes a plugin-relative resource path:
/util/table.als

module util/table
...


org.example.alloy.supertable.plugin depends on
org.example.alloy.table.plugin
and exposes a plugin-relative resource path: /util/supertable.als

How should I write supertable.als?

If I write:

module util/supertable
open util/table
...

A4 will certainly not find the table module because A4 doesn't know
anything about Eclipse plugins,
their locations and Eclipse URI schemes for portable references to
plugin resources:

platform:/plugin/org.example.alloy.table.plugin/util/table.als
platform:/plugin/org.example.alloy.supertable.plugin/util/supertable.als

In the current A4 API, it seems to me that all of the logic for mapping
module names to <ROOT>-relative or alloy4.jar-relative file names is,
fortunately, defined in one place:
edu.mit.csail.sdg.alloy4.Util.canon(String)

Is this correct?

Assuming it is, how about opening up this mechanism for API users to
replace the default mapping mechanism with another one?
For example, an Eclipse-aware mechanism could use
org.eclipse.core.runtime.FileLocator.toFileURL(URL) to let me write:

module util/supertable
open platform:/plugin/org.example.alloy.table.plugin/util/table.als
...


-- Nicolas.

Felix Chang wrote:

>
> On Sat, 5 Apr 2008, Nicolas Rouquette wrote:
> > Alloy3 had a module search path variable similar to Java's classpath.
> > This went away in Alloy4 which makes user-defined A4 specifications
> > location-dependent in contrast to A4's standard library and
> > book examples which are location-independent.
> >
> > This asymmetric handling of module names in 'open'
> > statements leads to a rather strange paradox, e.g:
> >
> > module foo -- specification foo is in ./foo.als
> > open util/relation -- ./util/relation.als is optional
> > open util/table -- ./util/table.als is required
> > open bar/baz -- ./bar/baz.als is required
>
> Dear Nicolas:
>
> Actually Alloy4's module inclusion mechanism is a bit more complicated.
> It is explained in bullet #9 in the "New Syntax" section of Alloy4
> Quickguide,
> but let me elaborate it with a full example.
>
> Suppose you have a "message.als" like this:
>
> module nicolas/project1/message
> open nicolas/project1/packet
> open nicolas/common/tcpip
>
> 1) The module line tells AlloyAnalyzer that message.als
> must reside at <ROOT>/nicolas/project1/message.als
> So if message.als is at /users/Nicolas/alloy/nicolas/project1/message.als,
> then Alloy Analyzer will infer that <ROOT> is /users/Nicolas/alloy
>
> 2) "open nicolas/project1/packet" means
> to load <ROOT>/nicolas/project1/packet.als
> In this case that means /users/Nicolas/alloy/nicolas/project1/packet.als
>
> 3) "open nicolas/common/tcpip" means
> to load <ROOT>/nicolas/common/tcpip.als
> In this case that means /users/Nicolas/alloy/nicolas/common/tcpip.als
>
> 4) There are two additional rules:
>
> 4a) If the "module" line is omitted in a particular ALS file,
> then we assume <ROOT> = the directory containing this ALS file.
>
> 4b) Alloy has a few useful libraries like "integer.als" and
> "ordering.als".
> Back in Alloy3 days, these were called "util/integer" and "util/ordering".
> So now, for compatibility reasons, when we see "open util/ordering",
> and you don't actually have such a file,
> then we assume you are referring to one of these util libraries.
>
> > This paradox induces an unfortunate consequence...
> > In turn, this induces a lot of duplication of A4 specifications.
> > For example, the relative path util/table.als must be valid in
> > each directory where it's referenced as 'open util/table'.
>
> Your claim that "The relative path ... must be valid in each ..." is
> incorrect.
> You just have to define the "module" line correctly.
>
> Suppose /home/project1/main.als says:
> module project1/main
> open util/table
> ...
>
> Suppose /home/project1/input/inputDriver.als says
> module project1/input/inputDriver
> open util/table
> ...
>
> Suppose /home/util/supertable.als says
> module util/supertable
> open util/table
> ...
>
> Suppose /home/util/table.als says
> module util/table
> ...
>
> Then main.als and inputDriver.als and supertable.als will ALL correctly
> import table.als, even though they are all at different locations
> in the file system.
>
> So what you fear does not happen: modules that import table.als
> do not need to all be at the same level in the file system,
> nor do you need to duplicate "table.als" multiple times in your file
> system.
>
> >
> > In Alloy3, there is support for a module search path variable in
> > alloy.util.FileUtil. Why was this removed in Alloy4?
> >
>
> I felt that the new automatic inferrence (when used correctly)
> should eliminate the need to fuzz with custom-defined search path
> variables.
>
> >
> > In Alloy4, there is a limited search path mechanism
> > to search for a module in the file system or in alloy4.jar.
> >
>
> This "search mechanism" is solely used to support the historical
> util/ordering util/integer util/relation library files...
> It is not intended and cannot currently be used by users
> to "resurrect" the Alloy3 search path variable mechanism.
>
> Sincerely,
> Felix Chang
> Alloy4 Developer
>
>  

[Felix Chang-2]

On Sun, 6 Apr 2008, Nicolas Rouquette wrote:

> org.example.alloy.table.plugin exposes
> a plugin-relative resource path: /util/table.als
> ...
> org.example.alloy.supertable.plugin... exposes
> a plugin-relative resource path: /util/supertable.als
>
> How should I write supertable.als?
>
> A4 will certainly not find the table module
> because A4 doesn't know anything about... Eclipse URI schemes

Dear Nicolas:

Indeed that is an interesting integration issue
between Alloy4 and Alloy4Eclipse.

>
> In the current A4 API, it seems to me that all of the logic for mapping
> module names to <ROOT>-relative or alloy4.jar-relative file names is,
> fortunately, defined in one place:
> edu.mit.csail.sdg.alloy4.Util.canon(String)
> Is this correct?
>

Yes.  Currently the canon() method recognizes two different formats:
(where '/' in the following paragraph refers to the platform's default
path separator, as indicated by Java's File.SEPARATOR property)

1) "/$alloy4$/something" means to get something from alloy4.jar
2) everything else means to get it from the local file system.

We can easily open it up to allow more formats, such as general URI.
But the current parser won't allow users to write the following:

>
> module util/supertable
> open platform:/plugin/org.example.alloy.table.plugin/util/table.als
>

That's because the argument to the OPEN statement must be  NAME [/ NAME]*
so it won't allow '.' or ':'.   And the parser will also fail on keywords.
For example, the following line will fail since "check" is an Alloy keyword:

    open platform/plugin/tablePlugin/check/interesting

There were previous proposals to allow OS-dependent quoted strings.
Perhaps allow the user to write something like

    open "../../abc/def.als"

I'll have to discuss these possible alternatives with Daniel,
and see what we come up with.

Sincerely,
Felix Chang
Alloy4 Developer

[Nicolas F Rouquette]

Hi Felix,

Alloy's beauty is its minimalistic syntax.
With URIs, not URLs, we don't even need quotes!

open <uri>

Clause 2.4.2 in the RFC 2396 spec says that a URL is *always* escaped!
(see: http://www.ietf.org/rfc/rfc2396.txt)

Then, all we need is for Util.canon to allow us to change the URI resolver
from module URI strings to java.io.File-compatible filenames, e.g.,
something like this:

class URIErr extends Err { ... }

interface AlloyModuleURIResolver {
    /* uri is an RFC-2396 URI which must be escaped and resolved to a
file */
    public (String?|File?) canon(String uri) throws URIErr;
}

// TODO: provide a mechanism to change the URI resolver, e.g.:
// - a static initializer that loads the resolver class based on a
system property class name
// - a static variable which can be changed at runtime

public static final (String?|File?) canon(String uri) throws URIErr {
    AlloyModuleURIResolver resolver = ...;
    return resolver.canon(uri);
}

The current implementation of Util.canon would then become the default
resolver.
Alloy4Eclipse could then use one of the Eclipse mechanisms for resolving
URIs, e.g.:

Alloy4 could run with the current URI-like resolution scheme for
handling URIs whose first segment is "$alloy4$"
and Alloy4Eclipse could switch to a different implementation that would
delegate the resolution to one of the Eclipse URI utilities, e.g.:

http://help.eclipse.org/help33/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/api/org/eclipse/core/filesystem/URIUtil.html

-- Nicolas.

Felix Chang wrote:

>
> On Sun, 6 Apr 2008, Nicolas Rouquette wrote:
> > org.example.alloy.table.plugin exposes
> > a plugin-relative resource path: /util/table.als
> > ...
> > org.example.alloy.supertable.plugin... exposes
> > a plugin-relative resource path: /util/supertable.als
> >
> > How should I write supertable.als?
> >
> > A4 will certainly not find the table module
> > because A4 doesn't know anything about... Eclipse URI schemes
>
> Dear Nicolas:
>
> Indeed that is an interesting integration issue
> between Alloy4 and Alloy4Eclipse.
>
> >
> > In the current A4 API, it seems to me that all of the logic for mapping
> > module names to <ROOT>-relative or alloy4.jar-relative file names is,
> > fortunately, defined in one place:
> > edu.mit.csail.sdg.alloy4.Util.canon(String)
> > Is this correct?
> >
>
> Yes. Currently the canon() method recognizes two different formats:
> (where '/' in the following paragraph refers to the platform's default
> path separator, as indicated by Java's File.SEPARATOR property)
>
> 1) "/$alloy4$/something" means to get something from alloy4.jar
> 2) everything else means to get it from the local file system.
>
> We can easily open it up to allow more formats, such as general URI.
> But the current parser won't allow users to write the following:
>
> >
> > module util/supertable
> > open platform:/plugin/org.example.alloy.table.plugin/util/table.als
> >
>
> That's because the argument to the OPEN statement must be NAME [/ NAME]*
> so it won't allow '.' or ':'. And the parser will also fail on keywords.
> For example, the following line will fail since "check" is an Alloy
> keyword:
>
> open platform/plugin/tablePlugin/check/interesting
>
> There were previous proposals to allow OS-dependent quoted strings.
> Perhaps allow the user to write something like
>
> open "../../abc/def.als"
>
> I'll have to discuss these possible alternatives with Daniel,
> and see what we come up with.
>
> Sincerely,
> Felix Chang
> Alloy4 Developer
>
>  

[Felix Chang-2]

On Wed, 9 Apr 2008, Nicolas Rouquette wrote:
> Alloy4 could run with the current URI-like resolution scheme
> for handling URIs whose first segment is "$alloy4$"
> and Alloy4Eclipse could switch to a different implementation that would
> delegate the resolution to one of the Eclipse URI utilities

Dear Nicolas:

On the API level, I think your suggestion is the right way to go.

> Clause 2.4.2 in the RFC 2396 spec says
> that a URL is *always* escaped!
> (see: http://www.ietf.org/rfc/rfc2396.txt)

On the parser level, allowing URI, even in the escaped form,
would mean allowing '%', ':', '.', and several other new characters.
I'll have to discuss with Daniel first.

Sincerely,
Felix Chang
Alloy4 Developer