What do the new `new` buttons do?

1

image
image1137×774 23.5 KB

What do “New Config/Trace/Init/Fork” do? Haven’t been able to figure out the differences through experimentation.

2

Nevermind think I got it

3

To sum it up:

  • New config yields a trace where the configuration (that is, the valuation of static parts) changed
  • New trace yields a new trace under the same configuration
  • New init yields a trace with a different initial state, under the same configuration
  • New fork yields a new trace which is similar to the current one until the currently-displayed state but differs afterwards.

The latter is very useful to check whether a different outcome is possible in a given state, e.g. if it’s possible to fire a different event than the one currently happening.

4

Followup question: what does the decompose strategy option do?

5

It analyses each configuration separately and concurrently. Can potentially speed up analysis a lot, in particular when using unbounded model checking.

6

I am working on the API for Alloy (again). I have to make an API for this traversal.

I think the navigation definitions map to the following tree navigation?

image
image550×562 22.2 KB

After you have a solution you can iterate over Instance objects. This then maps to calling the definition of config for each instance. I think there is always a finite set of instances associated with a solution?

Since a trace is always infinite, we cannot iterate over the State objects of a trace. I think we need a Instance.getTrace() method to give you a State object. This Trace object can then provide access to:

  • next() – the next State object, might point back.
  • prev() – The previous state, again, might be cyclic
  • fork() – Create a new trace that has the same State objects up to this.
  • init() – Create a new different State object based on a trace of the current Instance.

Would appreciate feedback on this … thanks.

7

Sorry, still trying to understand your model. What exactly are Instance objects in this perspective?

8

See org.alloytools.alloy/Alloy.md at feature/api · AlloyTools/org.alloytools.alloy · GitHub

I created a Solution interface and a Instance API since the Instance is useful in other contexts. Both the Instance and the Solution interfaces map to the old A4Solution class. I separated them because the Instance is quite useful in other contexts. As far as I can see, it can be passed as a bound to the solver?

A Solution was then Iterable over its instances. However, Alloy 6 now has the time trace … this adds another dimension in the navigation.

In the mean time I’ve done some more thinking and came up with the following API on Solution:

    /**
     * Return an iterator over the instances. Each instance is a configuration
     * instance, i.e. only the static parts are resolved. Since resolving is
     * expensive in time, the solutions should be fetched when needed and not
     * earlier. The actual resultion generally takes place when calling
     * {@link Iterator#hasNext()}.
     *
     * @return An iterator over the configuration instances.
     */
    Iterator<Instance> iterator();

    /**
     * Each configuration instance is associated with a Trace. A Trace is the graph
     * of instances where the last instance loops back to an earlier instance to
     * mimic an inifite trace.
     * <p>
     * This method creates a new Trace from a <em>current</em> Instance. An instance
     * can be a <em>configuration Instance</em> or a member of a Trace. It is
     * possible to iterate over all the traces associated with a configuration
     * instance , or over traces that share ancestor instances.
     * <p>
     * If the current Instance is a configuration INstance, then a Trace iterator
     * based on that configuration only return. This is the init button in the UI.
     * <p>
     * If current is a trace instance, the returned trace will share the same
     * ancestors as the current instance.
     *
     * @param current instance, either a configuration or a trace instance
     * @return an iterator over the traces of the current instance
     */
    Iterator<Trace> trace(Instance current);

    /**
     * Represents a trace. A trace is a set of instances over time. The last
     * instance loops back to an earlier instance.
     */
    interface Trace {

        /**
         * The sequence of instances
         */
        Instance[] instances();

        /**
         * Normally the instances are ordered by the array index. However, the last
         * instance loops back to the index returned here.
         */
        int loop();
    }

So mapping to the concepts of config, next, fork, and init.

    Iterator<Instance> it = solution.iterator();
    Instance configuration = it.nextElement();
    Iterator<Trace> inits = solution.trace(configuration);
    Iterator<Trace> forks = solution.trace(inits.next().instances[4]);

The words next, prev, fork, init, are tricky. I think it would be nice if we could standardize on proper terminology of the navigational axes.

  • configuration or static – This is the old Alloy <6 axis
  • trace, dynamic, or variable – This is the axis we have when the model contains variables

Thanks for the feedback. Would be nice if we could get this right.

9

Thanks for the clarification. The API is looking good, although I need to study it with a little more time.

What seems odd to me is that you separating the retrieval of the configuration from the traces. This makes sense conceptually, but the problem is that that’s not how the backend works: any solution returned by the solver already has a configuration and a trace associated.

10

The beauty of API’s! :slight_smile: When I design an API my concern is with the caller and then I later figure out how to make it work.

In the implementation it does require a special flag but it is pretty straightforward.

Thanks for the reply.