Date: Sat, 5 Apr 2008 21:09:39 -0400 (EDT)
From: Felix Chang

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 /nicolas/project1/message.als
So if message.als is at /users/Nicolas/alloy/nicolas/project1/message.als,
then Alloy Analyzer will infer that  is /users/Nicolas/alloy

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

3) "open nicolas/common/tcpip" means
to load /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  = 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

Date: Sun, 06 Apr 2008 17:08:38 -0700
From: Nicolas 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
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 -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
...

Date: Wed, 9 Apr 2008 21:28:11 -0400 (EDT)
From: Felix Chang

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

Date: Wed, 09 Apr 2008 23:44:25 -0700
From: Nicolas 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...

-- Nicolas.

Date: Thu, 10 Apr 2008 06:34:08 -0400 (EDT)
From: Felix Chang

> 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