Hello,

We are trying to simulate architectural design using the Alloy Analyzer. The architecture meta-model has been manually translated into Alloy code. An architecture design model (expressed in EMF) is transformed into Alloy code, which conforms to the meta-model expressed in Alloy code. The traces pattern (as found in http://alloy.mit.edu/alloy4/tutorial/s4_dynamic.pdf) is used to generate all the possible traces over the architecture, given an initial state. Unfortunately, we're running into tractability problems.

In our case, a single state represent the location of all the data in the architecture. These locations can be ports of components, or data instances which can hold data. A port can (in our simulation) hold only one concrete data value, while data instances can hold multiple. The
(simplified) State signature used is as follows:
sig State {
   next: lone State,
   portValues: Port -> lone Data,
   dataInstanceValues: DataInstance -> Data }

Given the large number of ports in the architecture (> 15), the number of possible states is enormous. Combine this with a large number of States for each trace (> 15), and simulation of the architecture becomes very time-consuming.

A single transition function is defined, which specifies the end-result of events from a given state, to a new state. Basically, it specifies that data is moved from one port to another port, if they are connected.
This is combined with some other expressions, which defined the 'inner-workings' of the components (such as storing data received from a port in a data instance).

It should be stated that the architecture itself is static, while only the data within the architecture is dynamic. For example, signatures for each component and port seem - at least to us - fairly restrictive. As an example:
(Meta-model)
enum PortDirection { ... }
abstract sig Port {
   direction: one PortDirection,
}
abstract sig DataPort extends Port {
   dataType: one DataType,
}

(Model)
one sig Port1 extends DataPort {
} {
   dataType = DT1
   direction = PortDirection_In
}

Can you give any hints on how to optimize the simulation? You are probably not able to give any domain specific optimizations, but hopefully you are able to give generic optimizations. We are trying to keep as much detail from the original architecture, and not remove(abstract) certain elements for the completeness of the simulation.

The untractability seems to come form the fact that the whole trace (with its states) is generated at once. A more iterative way (such as 'generating' a single new state from an single old state) seems to be the solution here. Is there any way to force Alloy/the SAT solvers into behavior such as this?