Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2015 / Formale Spezifikation und Verifikation / Uebungen / SortnetBDD.java


Inhaltsbereich

SortnetBDD.java

Java source code icon SortnetBDD.java — Java source code, 4 KB (4328 bytes)

Dateiinhalt

import bdd.BDDOperations;
import static bdd.BDDOperations.*;
import bdd.BDDVar;
import net.sf.javabdd.BDD;

import java.util.List;
import java.util.LinkedList;

public class SortnetBDD {
    
    static boolean isset(BDD set, BDDVar var){
        return (!((and(set,var(var))).isZero()));
    }

    public static void main(String[] args) /*throws TimeoutException*/ {
        //  int[][] net = {{1,3},{0,2},{2,3},{0,1},{1,2}};
        //  int[][] net = {{1,2},{0,1},{2,3},{0,2},{1,3}};
        //  int wires = 4;

        //  int[][] net = {{2,3},{3,4},{5,6},{6,7},{9,10},{10,11},{13,14},{14,15},{15,16},{16,17},{17,18},{18,19},{0,2},{1,3},{3,5},{4,6},{6,8},{7,9},{11,13},{12,14},{13,15},{14,16},{15,17},{16,18},{0,3},{2,5},{5,8},{7,10},{8,11},{9,12},{10,13},{11,14},{12,15},{13,16},{14,17},{15,18},{2,6},{3,7},{4,8},{5,9},{6,10},{7,11},{8,12},{9,13},{10,14},{11,15},{12,16},{14,18},{15,19},{0,7},{1,8},{4,11},{5,12},{2,15},{1,5},{2,6},{4,8},{5,9},{7,11},{8,12},{11,15},{12,16},{0,12},{0,6},{1,7},{3,9},{4,10},{6,12},{10,16},{13,19},{1,4},{2,5},{3,6},{4,7},{5,8},{6,9},{7,10},{8,11},{9,12},{10,13},{11,14},{12,15},{13,16},{16,19},{0,2},{1,3},{2,4},{3,5},{4,6},{5,7},{6,8},{7,9},{8,10},{9,11},{10,12},{11,13},{12,14},{13,15},{14,16},{15,17},{16,18},{17,19},{2,3},{4,5},{5,6},{6,7},{7,8},{9,10},{10,11},{11,12},{13,14},{16,17},{0,1},{1,2},{2,3},{3,4},{4,5},{5,6},{6,7},{8,9},{9,10},{10,11},{12,13},{14,15},{15,16},{17,18},{18,19}};
        int[][] net = {{17,18},{16,17},{14,15},{13,14},{8,9},{6,7},{2,3},{0,7},{1,8},{4,11},{6,13},{9,16},{12,19},{0,2},{1,3},{3,5},{5,7},{7,9},{8,10},{11,13},{12,14},{13,15},{14,16},{15,17},{17,19},{1,17},{2,18},{0,8},{3,11},{4,12},{6,14},{9,17},{2,6},{3,7},{4,8},{8,12},{9,13},{10,14},{11,15},{12,16},{14,18},{12,19},{10,17},{9,16},{5,12},{1,8},{0,7},{1,3},{4,6},{9,11},{12,14},{13,15},{14,16},{16,18},{17,19},{1,6},{2,7},{3,8},{4,9},{6,11},{7,12},{8,13},{10,15},{11,16},{12,17},{14,19},{0,8},{3,11},{5,13},{8,16},{0,3},{1,4},{2,5},{4,7},{5,8},{6,9},{7,10},{8,11},{9,12},{10,13},{11,14},{13,16},{14,17},{15,18},{0,6},{3,9},{2,6},{3,7},{5,9},{6,10},{8,12},{10,14},{18,19},{16,17},{15,16},{14,15},{13,14},{12,13},{11,12},{10,11},{9,10},{8,9},{7,8},{6,7},{5,6},{4,5},{3,4},{2,3},{1,2},{0,1},{1,2},{2,3},{3,4},{4,5},{5,6},{6,7},{7,8},{8,9},{9,10},{10,11},{11,12},{12,13},{13,14},{14,15},{15,16},{16,17},{17,18}};
        int wires = 20;

        int times = net.length;
        BDDVar[][] vars = new BDDVar[wires][2];
        List<BDDVar> zeros = new LinkedList<BDDVar>();
        List<BDDVar> ones = new LinkedList<BDDVar>();
        for(int i=0; i<wires; i++){
            zeros.add(vars[i][0] = freshBDDVar());
            ones.add(vars[i][1] = freshBDDVar());
        }

        BDD reaches = constantTrue();
        for(int t=0; t<times; t++){
            BDD thisnext =
                and(
                    iff(var(vars[net[t][0]][1]),or(var(vars[net[t][0]][0]),var(vars[net[t][1]][0]))),
                    iff(var(vars[net[t][1]][1]),and(var(vars[net[t][0]][0]),var(vars[net[t][1]][0])))
                    );
            for(int n=0; n<wires; n++){
                if(n!=net[t][0] && n!=net[t][1]){
                    thisnext = and(thisnext, iff(var(vars[n][0]), var(vars[n][1])));
                }
            }
            reaches = and(thisnext, reaches);
            reaches = exist(zeros, reaches);
            reaches = replace(reaches, ones, zeros);
            System.out.print("Nach diesem Komparator verbleiben an Sortierungen: ");
            System.out.println(reaches.satCount()/Math.pow(2.,wires));
        }

        BDD unsort = constantFalse();
        for(int n=0; n<wires-1; n++){
            unsort = or(and(neg(var(vars[n][0])),var(vars[n+1][0])), unsort);
        }

        BDD f = and(reaches,unsort);

        BDD setting = f.satOne();

        if (setting.isZero()) {
            System.out.println("Sortiernetzwerk ist korrekt.");
        } else {
            System.out.print("Sortiernetzwerk ist nicht korrekt.\n" +
                             "Folgende unsortierte Ausgabe kann erzeugt werden:\n");
            for(int n=0; n<wires; n++){
                if(isset(setting,vars[n][0])){
                    System.out.println("1");
                }else{
                    System.out.println("0");
                }
            }
        }
    }
}

Artikelaktionen


Funktionsleiste