Commit 873b4f2c authored by Alfons Laarman's avatar Alfons Laarman

Export ICE matrix

parent 518bde9e
package spins.promela.compiler.ltsmin;
import static spins.promela.compiler.Specification._NR_PR;
import static spins.promela.compiler.ltsmin.LTSminPrinter.MDS_DM_NAME;
import static spins.promela.compiler.ltsmin.LTSminPrinter.MES_DM_NAME;
import static spins.promela.compiler.ltsmin.LTSminPrinter.ICE_DM_NAME;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.assign;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.chanLength;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.decr;
......@@ -506,11 +509,10 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
/**
* MUST DISABLE
*/
static final String MDS = "dm_must_disable";
private static int generateMDSMatrix(LTSminModel model, GuardInfo guardInfo) {
int nlabels = guardInfo.getNumberOfLabels();
DepMatrix mds = new DepMatrix(nlabels, model.getTransitions().size());
guardInfo.setMatrix(MDS, mds, true);
guardInfo.setMatrix(MDS_DM_NAME, mds, true);
int disables = 0;
for (int g = 0; g < mds.getNrRows(); g++) {
LTSminGuard guard = (LTSminGuard) guardInfo.get(g);
......@@ -528,11 +530,10 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
/**
* MUST ENABLE
*/
static final String MES = "dm_must_enable";
private static int generateMESMatrix(LTSminModel model, GuardInfo guardInfo) {
int nlabels = guardInfo.getNumberOfLabels();
DepMatrix mes = new DepMatrix(nlabels, model.getTransitions().size());
guardInfo.setMatrix(MES, mes, true);
guardInfo.setMatrix(MES_DM_NAME, mes, true);
int disables = 0;
for (int g = 0; g < mes.getNrRows(); g++) {
LTSminGuard guard = (LTSminGuard) guardInfo.get(g);
......@@ -1075,7 +1076,7 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
int nlabels = guardInfo.getNumberOfLabels();
int neverICoEnabled = 0;
DepMatrix ico = new DepMatrix(nlabels, nlabels);
guardInfo.setICoMatrix(ico);
guardInfo.setMatrix(ICE_DM_NAME, ico, true);
DepMatrix g2g = model.getGuardInfo().getMatrix(G2G);
for (int g1 = 0; g1 < nlabels; g1++) {
Expression ge1 = guardInfo.get(g1).getExpr();
......
......@@ -119,6 +119,9 @@ public class LTSminPrinter {
public static final String COMMUTES_DM_NAME = "commutes_dm";
public static final String NES_DM_NAME = "nes_dm";
public static final String NDS_DM_NAME = "nds_dm";
public static final String MES_DM_NAME = "dm_must_enable";
public static final String ICE_DM_NAME = "dm_mce_invert1";
public static final String MDS_DM_NAME = "dm_must_disable";
public static final String GM_TRANS_NAME = "gm_trans";
public static final int STATE_ELEMENT_SIZE = 4;
public static final String SCRATCH_VARIABLE = "__spins_scratch";
......
......@@ -14,6 +14,7 @@ import java.util.Map.Entry;
import spins.promela.compiler.expression.Expression;
import spins.promela.compiler.ltsmin.LTSminTreeWalker.Options;
import static spins.promela.compiler.ltsmin.LTSminPrinter.*;
import spins.promela.compiler.ltsmin.matrix.DepMatrix;
import spins.promela.compiler.ltsmin.matrix.LTSminGuard;
import spins.promela.compiler.ltsmin.util.CNF;
......@@ -59,8 +60,6 @@ public class GuardInfo implements Iterable<Entry<String, LTSminGuard>> {
*/
private DepMatrix co_matrix;
private DepMatrix ico_matrix;
/**
* trans >
* trans ... ...
......@@ -183,11 +182,7 @@ public class GuardInfo implements Iterable<Entry<String, LTSminGuard>> {
}
public DepMatrix getICoMatrix() {
return ico_matrix;
}
public void setICoMatrix(DepMatrix ico) {
ico_matrix = ico;
return getMatrix(ICE_DM_NAME);
}
public List< List<Integer> > getTransMatrix() {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment