Baustellensim

Status
Nicht offen für weitere Antworten.

I need heelp

Mitglied
Hallo ich brauche Hilfe

In dieser Aufgabe soll der Verkehrsfluss auf eine Straße mit Baustellenampeln mittels synchronisierten Threads simuliert werden.
Aufgabe: Strasse Schreiben Sie eine Klasse Strasse, die eine Straße symbolisiert. Die Straße hat eine parametrierbare, aber danach für die Laufzeit der Simulation feste Länge (gemessen in Kilometern). Auf der Straße können beliebig viele Fahrzeuge fahren. Normalerweise hat die Straße zwei Fahrspuren (eine pro Richtung), sodass die Fahrzeuge in beide Richtungen ungehindert fahren können. Auf der gesamten Strecke herrscht Überholverbot, d. h. die Autos in einer Richtung können sich nicht gegenseitig überholen. Es kann weiterhin zu Engstellen kommen, an denen es nur eine Fahrspur gibt und daher abwechselnd immer nur die Autos aus der einen oder der anderen Richtung fahren können. Diese Engstellen werden von Ampeln reguliert.

Warum funktioniert das nicht ?





java.util.concurrent.ThreadLocalRandom;
Java:
import java.util.List;

class Auto {
    /*@ predicate auto(int p,int r)= position |-> p &*& richtung |->
     r &*& 0 < p &*& p < 5 &*& 0 < r &*& r < 5;
     @*/

    public int position;

    public int richtung;

    public Auto(int position, int richtung)
    //@ requires true;
    //@ ensures auto(?p,?r);
     {
         if(0<position&&position<5)
            this.position = position;
        else this.position=1;
        if(0<richtung&&richtung<5)
            this.richtung = richtung;
        else this.richtung=1;
    }

    public void drive(int ampel)
    //@ requires auto(?p,?r);
    /*@ ensures auto(?p2,r) &*& ampel!=Ampelstatus.GRUEN || p2!=r || ampel == Ampelstatus.GRUEN ;
    @*/
    {

        if (ampel == Ampelstatus.GRUEN) {
            this.position = richtung;
        }
    }

    public int getPosition()
    //@ requires auto(?p,?r);
    //@ ensures auto(p,r) &*& result==p;
    {
        return this.position;
    }

    public int getRichtung()
    //@ requires auto(?p,?r);
    //@ ensures auto(p,r) &*& result==r;
    {
        return this.richtung;
    }

    public String toString()
    {
        return "Auto [position=" + Richtung.getName(position) + ", richtung=" + Richtung.getName(richtung) + "]";
    }
}

Java:
class Richtung {
    final static int NORDEN = 1;

    final static int SUEDEN = 2;

    final static int WESTEN = 3;

    final static int OSTEN = 4;

    public static String getName(int key) {
        switch (key) {
        case 1:
            return "NORDEN";
        case 2:
            return "SUEDEN";
        case 3:
            return "WESTEN";
        case 4:
            return "OSTEN";
        default:
            return "";
        }
    }
}

Java:
class Ampelstatus {
    final static int ROT = 1;

    final static int GELB = 2;

    final static int GRUEN = 3;

    final static int GELBROT=4;

    public static String getName(int key) {
        switch (key) {
        case 1:
            return "ROT";
        case 2:
            return "GELB";
        case 3:
            return "GRUEN";
        case 4:
            return "GELBROT";
        default:
            return "";
        }
    }
}

Java:
class Ampel {
    /*@ predicate ampel(int s,int z) =
    status |-> s &*& zaehler |-> z &*&
    0 < s &*& s < 5 &*&
    0 <= z &*& z < 4 ;
    @*/
    private int status;

    private int zaehler;

    public Ampel(int status, int zaehler) {
        this.status = status;
        this.zaehler = zaehler;
    }

    private void changeStatus()
    //@ requires    ampel(?s,?z);
    /*@ ensures    ampel(?s2,z) &*&
    0 <= z || z<4 ||
    s==Ampelstatus.GELB && s2==Ampelstatus.GRUEN ||
    s==Ampelstatus.GRUEN && s2==Ampelstatus.GELBROT ||
    s==Ampelstatus.GELBROT && s2==Ampelstatus.ROT ||
    s==Ampelstatus.ROT && s2==Ampelstatus.GELB;
     @*/
    {
        switch (this.status) {
        case Ampelstatus.GRUEN:
            this.status = Ampelstatus.GELBROT;
            break;
        case Ampelstatus.GELB:
            this.status = Ampelstatus.GRUEN;
            break;
        case Ampelstatus.ROT:
            this.status = Ampelstatus.GELB;
            break;
        case Ampelstatus.GELBROT:
            this.status=Ampelstatus.ROT;
            break;
        }
    }

    public int getStatus()
    //@ requires ampel(?s,?z);
    //@ ensures ampel(s,z) &*& result==s;
    {
        return this.status;
    }

    public void addZaehler()
    //Kann nicht verifiziert werden wegen eines Fehlers in verifast
    {
        if (this.zaehler < 3) {
            this.zaehler++;
        } else {
            this.zaehler = 0;
            this.changeStatus();
        }
    }

    public String toString() {
        return "Ampel [status=" + Ampelstatus.getName(status) + ", zaehler=" + zaehler + "]" ;
    }
}

Java:
class Strasse {
    /*@ predicate strasse(Auto a,int p,Ampel am, int r) =
    auto |-> a &*& position |-> p &*& ampel |-> am &*& richtung |-> r &*&
    a != null &*&
    0 < p &*& p < 5 &*&
    am != null &*&
    0 <= r &*& r < 2;
    @*/

    /*@
    predicate strasseOhneAuto(int p,Ampel am,int r)=
    position |-> p &*& ampel |-> am &*& richtung |-> r &*&
    0 < p &*& p < 5 &*&
    am != null &*&
    0 <= r &*& r < 2;
    @*/
    private Auto auto;

    private int position;

    private Ampel ampel;

    private int richtung;

    public Strasse(int position, Ampel ampel) {
        this.position = position;
        this.ampel = ampel;
        this.richtung=0;
    }

    private void addAuto()
    //@ requires strasseOhneAuto(?p,?am,?r) &*& this.auto |-> _;
    //@ ensures strasse(?a2,?p2,?am2,?r);
     {
        int autoRichtung=0;
        switch (position) {
        case Richtung.NORDEN:
            autoRichtung=this.richtung==0?Richtung.SUEDEN:Richtung.WESTEN;
            break;
        case Richtung.SUEDEN:
            autoRichtung=this.richtung==0?Richtung.NORDEN:Richtung.OSTEN;
            break;
        case Richtung.WESTEN:
            autoRichtung=this.richtung==0?Richtung.SUEDEN:Richtung.OSTEN;
            break;
        case Richtung.OSTEN:
            autoRichtung=this.richtung==0?Richtung.NORDEN:Richtung.WESTEN;
            break;
        }

        Auto auto = new Auto(this.position, autoRichtung);
        assert auto != null;
        this.richtung=this.richtung==1?0:1;
        this.auto = auto;
    }

    //requires strasseOhneAuto(?p,?am,?lp) &*& this.auto |-> _;
    // ensures strasse(?a,?p2,?am2,?lp2);
    public void tick()
    {
        if (this.auto == null) {
            this.addAuto();
        } else if (this.auto.getPosition() != this.position) {
            this.addAuto();
        }
        this.ampel.addZaehler();
        this.auto.drive(this.ampel.getStatus());
        System.out.println(this.toString());
    }

    public String toString() {
        return "Strasse [auto=" + this.auto.toString() + ", position=" + Richtung.getName(position) + ", ampel="
                + ampel.toString() + "]";
    }
}

Java:
class Simulation {
    /*@ predicate simulation(Strasse[] s)=
    strassen[0..strassen.length] |-> s &*&
    forall_ (int k;k <0 || k >= s.length || nth(k,s)!= null);
    @*/
    private Strasse[] strassen;

    public Simulation() {
        super();
        this.strassen = new Strasse[4];
    }

    public void init() {
        Ampel ampel = new Ampel(Ampelstatus.GRUEN, 0);
        Ampel ampel2 = new Ampel(Ampelstatus.GRUEN, 0);
        Ampel ampel3 = new Ampel(Ampelstatus.ROT, 0);
        Ampel ampel4 = new Ampel(Ampelstatus.ROT, 0);
        strassen[1] = new Strasse(Richtung.NORDEN, ampel2);
        strassen[3] = new Strasse(Richtung.OSTEN, ampel4);
        strassen[0] = new Strasse(Richtung.SUEDEN, ampel);
        strassen[2] = new Strasse(Richtung.WESTEN, ampel3);
    }

    public void start() {
        java.util.Scanner in = new java.util.Scanner(System.in);
        String stop = "";
        while (!"stop".equals(stop)) {
            for (int i = 0; i < strassen.length; i++) {
                strassen[I].tick();
            }
            stop = in.nextLine();
        }
        in.close();
    }
 
Zuletzt bearbeitet von einem Moderator:
Status
Nicht offen für weitere Antworten.

Neue Themen


Oben