A problem occurs with method calls such as this.m() since m has accessed to every field of this (see #2).
To allow non-static methods in a spacetime module, we can etiher:

1. Analyse the Java method to check for read and write accesses (seems very complex since we must parse and understand the full Java syntax).
2. Annotate the call on this with the permissions of the variables accessed.
3. Allow possible causality holes when calling external functions (i.e. Java methods).

Consider the following program:

module Depth depth = new Depth();
depth.count()

The depth counter will never be increased because we call depth.count() instead of run depth.count().

If we accept classes with same name (but in different package), we need a package resolution mechanism that look up into the import list.
It is not easy with little benefit for now so the solution is to forbid bonsai class to have an identical name.

Problem: Calling a method this.m() means that m has accessed to every field of this and we cannot control which ones are accessed and how.

Solution: Add a static analysis to prevent non-static method in spacetime modules.

See also #3.

Perform the causality analysis of the processes starting from the roots of the DAG and tagging the processes explored.

  public proc bug() =
    single_space LMax depth = 2;
    System.out.println(depth.value);
  end

with assert:

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `Spacetime(SingleSpace)`,
 right: `Host`: depth', src/middle/resolve.rs:76:9

NOTE: the code above is not right anyway since value is private in LMax. However it should be triggered at the Java compilation stage, not at the Bonsai compilation stage.

The compiler just reports that a causality analysis occurred without giving information on the variables that generate this error.
This is a well-known weakness of constraint programming: it is hard to debug (or in this case explain) unsatisfiable instances.
There exists however a bunch of techniques, references and techniques can be found in Chapter 6 of "Making the Most of Structure in Constraint Models", Kevin Leo, 2018.
We could also take advantage of the iterative structure of our problem by testing the satisfiability each time we add a constraint into the model.

For example: pre x.inc() should not be valid because the method inc modifies the variable x.

We chose to specify read/write attributes on the variables because we did not want to impact the Java signature of a method (that might not be inside the current project) or add wrappers around these methods to specify these attributes.
However this static analysis would be more easily done if we have read/write attributes on the methods themselves.
Another possibility is to force the user to write pre read x.inc() although with pre it is already implied.
(Note that it does not solve the problem that the user can lie about the Java signature...).