strassensimulation

I need heelp · 9. Nov 2017

Hallo ich brauche hilfe bei meiner aufgabe ich soll eine ampel erstellen mit threads die rot und grün schaltet mein ansatz befindet sicj im anhang

SchwarzWeiß · 9. Nov 2017

Füge den Code lieber mit Code-Tags (Symbolleiste -> Einfügen -> Code -> Sprache: Java) hinzu anstatt als Anhang, dann wird man dir schneller helfen können

Die Attribute solltest du als private deklarieren.
Was stellt denn das Attribut "zustand" dar?

truesoul · 9. Nov 2017

Hallo.
Ja aber bei was brauchst du Hilfe? Irgendwelche Fragen?

Grüße

VfL_Freak · 9. Nov 2017

Moin,

auch wenn Dui keine konkreten Fragen gestellt hast: nett wäre bspw. eine Main-Funktion !!

VG Klaus

I need heelp · 10. Nov 2017

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();
    }

SchwarzWeiß · 10. Nov 2017

Jetzt noch den Start-Tag am Code-Anfang hinzufügen, so wird sich das keiner anschauen...

I need heelp · 10. Nov 2017

Was ist damit gemeint ?

SchwarzWeiß · 10. Nov 2017

Java:

[code=java]

an den Code-Anfang schreiben

I need heelp · 10. Nov 2017

Java:

java.util.concurrent.ThreadLocalRandom;

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) + "]";

}


}


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 "";

}

}


}


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 "";

}

}

}


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 + "]" ;

}


}


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() + "]";

}


}


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.tick();

}

stop = in.nextLine();

}

in.close();

}

[/code=java]

Joose · 10. Nov 2017

@I need heelp ich habe deinen Beitrag entsprechend formatiert. Jede Klasse ist in einem eigenen Code Block und ich habe unnötige Leerzeilen entfernt.
Das ist übersichtlicher als ein großer Code Block und die ganzen Leerzeilen unterbrechen nur den Lesefluss und machen den Beitrag unnötig lang.

VfL_Freak · 10. Nov 2017

Moin,

I need heelp hat gesagt.:
Warum funktioniert das nicht ?

und was erwartest Du jetzt??

Lies bitte mal dies hier durch: http://www.java-forum.org/forum-faq-beitraege/7407-man-fragen-richtig-stellt.html

Danke und VG
Klaus

I need heelp · 10. Nov 2017

Diese Aufgabe ist sehr wichtig für mich bitte nur weiterhelfende Kommentare nicht zum runter machen danke für sowas ist ein forum nicht da

Anscheinend hab ich fehler drin das programm stürzt ab

Robat · 10. Nov 2017

I need heelp hat gesagt.:
Anscheinend hab ich fehler drin das programm stürzt ab

Kommt eine Exception (Fehlermeldung)? Wenn ja poste bitte den Stacktrace + dazugehörigen Code(zeilen)

I need heelp · 10. Nov 2017

Die fehler meldung lautet public static void main oder eine JavaFX-Anwendung muss javafx.application.Application erweitern

SchwarzWeiß · 10. Nov 2017

Dann zeig uns doch mal die Klasse mit der main-Funktion

I need heelp · 10. Nov 2017

Genau das ist mein problem die klasse simulation soll alles steuern nur hab ich da die main hin wurde nicht akzeptiert

SchwarzWeiß · 10. Nov 2017

Geb mal wie Robat schon gesagt hat den ganzen Stacktrace an, so verstehe ich nicht, was das ganze mit JavaFX zu tun haben soll.

Xyz1 · 10. Nov 2017

Java-Tags (auch in PNs) verwenden, habe ich der TE auch in einer PN geschrieben (als Antwort auf eine Anfrage der TE hin) und wie das geht steht auch in meiner Siggi - und BEIDES wurde ignoriert. Ich gehe nicht davon aus, dass diese Frage echt ein Anliegen ist.
Schau dich um, wie man Fragen richtig stellt - und erwarte am besten keine Komplettlösung.

I need heelp · 10. Nov 2017

Wenn ich komplett lösungen.erwarten würde hätte ich mein programm nicht selbst gechrieben und nach fehlern gefragt

Xyz1 · 10. Nov 2017

Ok, fangen wir damit an. Wenn die Ampeln eine Position (auf der Straße) haben, dann müssten Fahrzeuge doch auch eine Position auf der Straße haben. Außerdem... Ist ein Raster/Gitternetz gefragt?
Wie würdest du es modellieren?
Und überhaupt, Fahrzeuge müssten sich doch auch bewegen, ihre Geschwindigkeit ändern, stehenbleiben, anfahren, usw. Und sollen sie spawnen?
Mal wirklich jetzt; Straße, Ampel, Auto; drei große Fragezeichen, welche Gedanken hast du dir drum gemacht?

Joose · 10. Nov 2017

I need heelp hat gesagt.:
.... bitte nur weiterhelfende Kommentare nicht zum runter machen danke für sowas ist ein forum nicht da

Aber um dir helfen zu können musst du eben die passenden Informationen liefern. Einfach nur Code posten, eine kleine Beschreibung was verlangt ist und sagen "es funktioniert nicht" ist nicht zielführend.

Den Code hast du schon geliefert. Aber keine Fehlerbeschreibung bzw. welche Verhalten du dir erwünscht. Außerdem ist es auch hilfreich was du schon probiert hast um den Fehler zu fixen, damit nicht der gleiche Vorschlag nochmal kommt

I need heelp hat gesagt.:
Die fehler meldung lautet public static void main oder eine JavaFX-Anwendung muss javafx.application.Application erweitern

Poste einfach die Fehlermeldung

I need heelp hat gesagt.:
Genau das ist mein problem die klasse simulation soll alles steuern nur hab ich da die main hin wurde nicht akzeptiert

Dann füge der Klasse "Simulation" eine main-Methode hinzu. Was wurde nicht akzeptiert? Welche Fehlermeldungen sind gekommen?

strassensimulation

Mitglied

Anhänge

Bekanntes Mitglied

Top Contributor

Top Contributor

Mitglied

Bekanntes Mitglied

Mitglied

Bekanntes Mitglied

Mitglied

Top Contributor

Top Contributor

Mitglied

Top Contributor

Mitglied

Bekanntes Mitglied

Mitglied

Bekanntes Mitglied

Xyz1

Gast

Mitglied

Xyz1

Gast

Top Contributor