SCryptoDiagnoser is a Model-Based Diagnosis solver based on SAT described in the paper
"Compiling Model-Based Diagnosis to Boolean Satisfaction".
SCryptoDiagnoser approach is constraint-based and it generating a constraint model for the instance,
compiling the constraints to CNF using
BEE and solving the CNF using
SCryptoMinisat.
SCryptoDiagnoser
SCryptoDiagnoser is a tool which process the System and find Top-Level Minimal Cardinality Diagnoses.
This tool is using
BEE and
SCryptoMinisat and written in Prolog.
SCryptoDiagnoser Usage
Executation command
> SCryptoDiagnoser <system id> <observations set> [<limit solutions>]
By executing the above the solver will try to load preprocessed system file: "./data/<system id>.syspp".
If failed it will load system file: "./data/<system id>.sys" , preprocess it and save it to "./data/<system id>.syspp".
Then it will load observations set file: "./data/<system id>_<observations set>.obs"
and will find minimal cardinality top-level diagnoses for each observation in the obsercations set file.
For each observation it will find at most <limit solutions> top-level diagnoses and save them into
"./output/<system id>_<observations set>_<observation id>.tld" files.
(Note: <limit solutions> is optinal. By not declaring or assign to 0 the solver will search for all minimal cardinality top-level diagnoses).
Example
Solving all system "c17" observations from ISCAS85 benchmark and limit the amount of TLD to 2:
> SCryptoDiagnoser c17 iscas85 2
sys,set,obs,bound,MC,MC Time,TL Cnt,TL Time
c17,iscas85,1,2,1,0.0599999,2,0.072,done
c17,iscas85,2,1,1,0.000999928,1,0.00300002,done
....
c17,iscas85,62,2,2,0.00100017,2,0.00700021,done
c17,iscas85,63,2,2,0.000999928,2,0.00699997,done
and will generate the minimal cardinality top-level diagnoses files:
./output/c17_iscas85_1.tld
...
./output/c17_iscas85_63.tld
SCryptoDiagnoser Output
SCryptoDiagnoser prints to the standard ouput tabular information. It is in Comma-Separated Values format.
The columns description:
sys - System ID
set - Observation set ID
obs - Observation ID
bound - The upper-bound found on the minimal cardinality.
MC - The minimal cardinality found.
MC Time - The time took to find a minimal cardinality diagnosis.
TL Cnt - The amount of Top-Level diagnoses found.
TL Time - The total time took to find the Top-Level diagnoses.
SCryptoDiagnoser TLD2ALL
SCryptoDiagnoser TLD2ALL is a tool which expands Top-Level Diagnoses found by ScryptoDiagnoser to all Diagnoses.
This tool implements Procedure 2 from the
paper and written in Java.
SCryptoDiagnoser TLD2ALL Usage
After executing ScryptoDiagnoser to find Top-Level Diagnoses which processed the system, saved the processed system description to a .syspp file and saved the Top-Level Diagnoses to a .tld files,
SCryptoDiagnoser TLD2ALL will expand each of the Top-Level Diagnosis to all the diagnoses it represents in polynomial time.
For each Top-Level Diagnoses file it will find all the diagnoses it represents and save them into
"./output/<system id>_<observations set>_<observation id>.all" files.
Executation command
> java -jar tld2all.jar -embedded <system id> <observations set>
Example
Solving all system "c17" observations from ISCAS85 benchmark using SCryptoDiagnoser:
> SCryptoDiagnoser c17 iscas85
...
Expand the Top-Level diagnoses found by SCryptoDiagnoser for observaions set to all diagnoses using TLD2ALL:
> java -jar tld2all.jar -embedded c17 iscas85
Read preprocessed system time: 6 ms.
-------------------------
sys,set,obs,allcnt,alltime,ttltime
c17,iscas85,1,2,0.0020,0.0080
...
c17,iscas85,61,7,0.0010,0.0070
c17,iscas85,62,5,0.0010,0.0070
c17,iscas85,63,6,0.0010,0.0070
SCryptoDiagnoser TLD2ALL Output
SCryptoDiagnoser TLD2ALL prints to the standard ouput tabular information. It is in Comma-Separated Values format.
The columns description:
sys - System ID
set - Observation set ID
obs - Observation ID
allcnt - Total amount of diagnoses found.
alltime - Time to find all diagnoses from Top-Level diagnoses.
ttltime - Time to find all diagnoes including the time to load the preprocesed system.
File Formats
SCryptoDiagnoser is written in Prolog and therefore the file formats written in Prolog style.
System Description (.sys)
File Format
<System ID>.
[<List of System inputs>].
[<List of System outputs>].
[<List of System gates>].
Where
System gate = [<gate logic type>,<gate ID>,<gate output>,<gate input 1>,...,<gate input n>]
Gate logic type ∈ {buffer,inverter,and<I>,or<I>,nand<I>,nor<I>,xor<I>}
<I> is the amount of gate inputs.
Example
System 74182 description file:
74182.
[i1,i2,i3,i4,i5,i6,i7,i8,i9].
[o1,o2,o3,o4,o5].
[[inverter,gate49,z1,i9],
[or4,gate53,o1,i1,i3,i5,i7],
[and4,gate54,z2,i2,i4,i6,i8],
[and4,gate55,z3,i5,i2,i4,i6],
[and3,gate56,z4,i3,i2,i4],
[and2,gate57,z5,i1,i2],
[or4,gate58,o2,z2,z3,z4,z5],
[and4,gate59,z6,i4,i6,i8,z1],
[and4,gate60,z7,i7,i4,i6,i8],
[and3,gate61,z8,i5,i4,i6],
[and2,gate62,z9,i3,i4],
[nor4,gate63,o3,z6,z7,z8,z9],
[and3,gate64,z10,i6,i8,z1],
[and3,gate65,z11,i7,i6,i8],
[and2,gate66,z12,i5,i6],
[nor3,gate67,o4,z10,z11,z12],
[and2,gate68,z13,i8,z1],
[and2,gate69,z14,i7,i8],
[nor2,gate70,o5,z13,z14]].
Preprocessed System Description (.syspp)
File Format
<System ID>.
[<List of System inputs>].
[<List of System outputs>].
[<List of System gates sorted by depth from system inputs>].
[<List of System sections>].
[<List of System cones>].
Where:
System gate = (<gate ID>,<gate output>,<list of gate inputs>,<gate logic type>,<gate type>)
System Section = (<section ID>,<list of section gates IDs>,<section upper-bound>)
System Cone = (<dominator gate ID>,<list of dominated gates IDs>)
Gate logic type ∈ { buffer,inverter,and,or,nand,nor,xor }
Gate type ∈ { dominator, dominated, free }
Example
Preprocessed System 74182 description file:
74182.
[i1,i2,i3,i4,i5,i6,i7,i8,i9].
[o1,o2,o3,o4,o5].
[(gate49,z1,[i9],inverter,free),
(gate53,o1,[i1,i3,i5,i7],or,free),
(gate54,z2,[i2,i4,i6,i8],and,dominated),
(gate55,z3,[i5,i2,i4,i6],and,dominated),
(gate56,z4,[i3,i2,i4],and,dominated),
(gate57,z5,[i1,i2],and,dominated),
(gate60,z7,[i7,i4,i6,i8],and,dominated),
(gate61,z8,[i5,i4,i6],and,dominated),
(gate62,z9,[i3,i4],and,dominated),
(gate65,z11,[i7,i6,i8],and,dominated),
(gate66,z12,[i5,i6],and,dominated),
(gate69,z14,[i7,i8],and,dominated),
(gate58,o2,[z2,z3,z4,z5],or,dominator),
(gate59,z6,[i4,i6,i8,z1],and,dominated),
(gate64,z10,[i6,i8,z1],and,dominated),
(gate68,z13,[i8,z1],and,dominated),
(gate63,o3,[z6,z7,z8,z9],nor,dominator),
(gate67,o4,[z10,z11,z12],nor,dominator),
(gate70,o5,[z13,z14],nor,dominator)].
[(section1,[gate53],1),
(section2,[gate68,gate69,gate70],1),
(section3,[gate54,gate55,gate56,gate57,gate58],1),
(section4,[gate49],1),
(section5,[gate64,gate65,gate66,gate67],1),
(section6,[gate59,gate60,gate61,gate62,gate63],1)].
[(gate70,[gate68,gate69]),
(gate58,[gate54,gate55,gate56,gate57]),
(gate67,[gate64,gate65,gate66]),
(gate63,[gate59,gate60,gate61,gate62])].
Observations set (.obs)
File Format:
(<System ID>,<Observation ID>,[<Observation>]).
...
Example
Partial ISCAS85 observations for system 74182 file:
(74182,1,[i1,-i2,i3,i4,i5,i6,i7,i8,i9,-o1,-o2,-o3,-o4,-o5]).
(74182,2,[-i1,-i2,-i3,i4,-i5,-i6,-i7,-i8,-i9,-o1,-o2,-o3,o4,o5]).
(74182,3,[-i1,-i2,-i3,i4,-i5,-i6,i7,i8,i9,o1,o2,o3,o4,-o5]).
...
Top-Level Diagnoses (.tld)
File Format
<Observation as described above>
[<List of unhealthy gates IDs>].
...
Example
Two Top-Level Diagnoses for observation 231 of system 74182
(74182,231,[i1,-i2,i3,i4,i5,-i6,-i7,i8,i9,-o1,o2,o3,-o4,-o5]).
[gate70,gate67,gate63,gate58,gate53].
[gate67,gate58,gate49,gate53,gate63].
All Diagnoses (.all)
File Format
<Observation as described above>
Example
All Diagnoses for system 74182 observation #231
(74182,231,[i1,-i2,i3,i4,i5,-i6,-i7,i8,i9,-o1,o2,o3,-o4,-o5]).
[[gate70,gate69,gate68],[gate67,gate65,gate66,gate64],[gate63,gate62],[gate58,gate54,gate55,gate56,gate57],[gate53]].
[[gate67,gate65,gate66,gate64],[gate58,gate54,gate55,gate56,gate57],[gate49],[gate53],[gate63,gate62]].
The above describes 160 diagnoses for system 74182 observation #231 (3*4*2*5*1 + 4*5*1*1*2).
Notes
- For convenience of use, the solver archive file contains a batch file "SCryptoDiagAll" which
run SCryptoDiagnoser and SCryptoDiagnoser TLD2ALL one after the other and save the outputs to CSV files.
For usage see README file in the solver archive file.
- Searching for a single Minimal Cardinality diagnosis can be done by using only SCryptoDiagnoser
(limit the amount of solutions to 1).
- SCryptoDiagnoser TLD2ALL is a standalone tool which can be used to expand Top-Level diagnoses found by other algorithms.
Solver Downloads
SCryptoDiagnoser compiled with SWI Prolog 6.0.2.
Instances Downloads
Experiments Information Downloads