The code and binaries provided here implement a translator for diagnosability testing by SAT. Given a system model, given a number of steps n, it generates a CNF file that is satisfiable iff there exists a critical path that loops in less than n steps (which proves that the system is not diagnosable). The diagnosability testing is not performed by the software: an external SAT solver must be called (the problem is however saved in DIMACS format).
The parameters should be the following ones:
An example of use is the following one:
The late CSDL modeling language was used to model reconfigurable decentralised DES. The purpose of this section is not to provide a complete description of this language, but a sufficient one which, together with examples, should allow any interested user to write their own models. Courageous people should be able to read the parsers, provided in .g format (using AntLR technology).
A DES in CSDL is a set of interconnected components. Each component instantiates a component type described in a library. A connection is defined as a pair of ports from different components, which implicitly forces the simultaneous occurrence of shared events. An additional aspect of CSDL is the reconfiguration, which allows to add/remove components/connections, but this is ignored in the present software.
A component type is defined by a set of states variables, a set of ports, a set of events (associated with ports), and a set of transition rules. A state variables is associated with a domain, the first value of which is assumed to be the initial one (binary domains can make SAT methods more efficient). Ports are divided in input ports (from which messages are read), output ports (upon which messages are written), and a spontaneous port (from which messages are read). An event corresponds to the writting/reading of a message on a port. Finally, transitions are defined by the reading of a message (keyword when) in a state that satisfies a certain property (keyword require) which may change the state (keyword effect) and may lead to messages being written (keyword output).
The initial configuration (list of components, how they are connected, and what is observable) is given in a codl file, which should be self explanatory.
The variable loader is the object responsible for preventing conflicts with SAT variable. Certain parts of the software may allocate new SAT variables and are then responsible for remembering what these variables mean (generally throw a VariableAssigner, see below). File VariableLoader.java is located in package edu.supercom.util.sat.
In an attempt to keep the implementation clean, and to prevent a tight integration of the solver in the translator, the software only generates clauses that are transmitted to a clause stream. The clause stream is responsible for dealing with clauses it is given. In the provided implementation, the clause stream saves the clauses in a file. However, it would be possible to connect the clause stream to a SAT solver, or to use dedicated streams to output debugging messages.
The ClauseStream.java file is located in package edu.supercom.util.sat and contains the following methods:
A VariableAssigner is an object that returns the SAT variable (or literal) associated with some specified semantics. For instance, the variable assigner keeps the knowledge that the semantics event e takes place at time step 5 will be true iff the SAT variable 201 is true. This way, most SAT clauses are first defined in terms of semantics before being translated in SAT literals.
Class VariableAssigner.java is located in package edu.supercom.util.sat together with VariableSemantics.java. Most semantics implementations can be found in package edu.supercom.diag.sat.sem.
Non diagnosability is proved by finding a path on the twin plant. The SAT problem associated with this question is therefore a collection of constraints on this path (for instance, the path must satisfy the model; it must produce an identical observation on both plants; etc.). These constraints are partitioned into path constraints.
File PathConstraint.java can be found in package edu.supercom.diag.sat and implementations in package edu.supercom.diag.sat.constraint. (In the current implementation, the path constraints are not allowed to allocate variables.)
At the moment, time steps are manipulated explicitly as integer. It is quite unconvenient, especially because one always need to remember whether the transition before (state) time step t and (state) time step t+1 takes place at (transition) time step t or (transition) time step t+1. I have a new implementation (not incorporated in this one) with explicit classes called StateTimeStep and TransTimeStep that I could put back in the code upon request.
The main file is ND.java located in package edu.supercom.diag.sat. It is hopefully quite readable and should provide insight as to how the software works.