D120.de/forum

mirko-koehler hat geschrieben: ↑

30. Okt 2017 15:03

Make sure to use quotation marks when running sbt in batch mode, i.e.

Code: Alles auswählen

sbt "submit <tu-id> <token>"

works for me.


Mirko

I have just tried it. Using quotation marks does the trick for me.

Thanks mirko-koehler and 0b101101101 for your help.

Hi all, I had problems with the submission of my solution of assignment 0. After some experimenting I have found out that the submit task only works from the interactive sbt console for me. If I type the following directly into my command prompt sbt submit <tu-id> <token> I get this error [error] [e...

Hallo, per Widerspruchsbeweis wird in den Folien gesagt, dass "while true do skip od" nicht terminiert, da der Zustand nach einem Schleifendurchlauf wieder der selbe ist. Wie würde man Beweisen, dass "while true do c od" nie terminiert? Man kann dann nicht sagen, dass o=o', wodurch man den Widerspr...

Kann ich das anhand von Einsetzen zeigen oder argumentiere ich einfach, das x im Zustand o'' zu 0 ausgewertet wird? Nur ganz kurz, du musst schon das Urteil \langle(x \oplus 1), \sigma''\rangle \Downarrow 1 herleiten. Das wird schließlich in der Prämisse der Regel r:= benötigt. Dort möchtest du, ja...

Gilt dann nach diesem Teil der Definition für: \{ s.t \space | \space s.(\checkmark) ∈ traces(P) ∧ t ∈ traces(Q)\} = \{ ((), \checkmark), (x, \checkmark) \} ? Das gilt nicht. Nehmen wir beispielsweise (x, \surd) \in \{s.t \space | \space s.(\surd) ∈ traces(P) ∧ t ∈ traces(Q)\} an. Es gibt jetzt dre...

Hallo, wir haben in Modul 1 auf Folie 15 das kartesische Produkt auf endlichen Folgen eingeführt. (Ich möchte an dieser Stelle anmerken, dass hier das intuitive Verständnis von endlichen Folgen vorausgesetzt wird, da endliche Folgen selber erst auf Folie 17 auf Basis der Definition von Folie 15 eing...

Ich glaube, mein Problem ist, dass ich nicht verstehe, wieso die Herleitung von while true do skip od endlich ist. Ich kann doch bis in alle Ewigkeit rwht anwenden, oder nicht? Natürlich ist das möglich, dennoch ist jede Herleitung selbst endlich lang. Um es hoffentlich etwas klarer zu machen: Es l...

Hallo, ich verstehe nicht ganz, warum die in Modul 7, Folie 11 definierte Relation für Com wohlfundiert ist. Existiert hier nicht ein ähnliches Problem wie bei der Strukturellen Induktion, nämlich, dass es bei der while-Schleife nicht unbedingt ein "kleinstes" Element gibt, denn die rwht-Regel könn...

In der Musterlösung wird diese Anordnung in der Definition der Menge REIHE erzwungen. Die prädikaktenlogischen Formel hat folgende Form: (\forall k \in h: \varphi_1 \vee \varphi_2) \wedge \varphi_3 \vee \varphi_4 \varphi_1 := (\exists k' \in h: \text{num-wert}(\text{wert}(k')) = \text{num-wert}(\tex...

Hallo, ich freue mich über das Interesse. Gerne können wir auch via Messenger diskutieren Über Messenger finde ich auch eine Superidee. Ich bin da 100% dabei Die Idee finde ich gut. Bisher gibt es noch keine Messenger-Gruppe, aber ich werde heute eine Skype-Gruppe erstellen. Schreibt mir am Besten e...

Hallo, in Vorbereitung auf die Klausur suche ich Interessierte für eine Lerngruppe. Das Ziel der Lerngruppe soll nicht das gemeinsame Bearbeiten von Aufgaben in Präsenz sein. Ich bin der Meinung, dass der Lerneffekt dann am höchsten ist, wenn jeder die Aufgaben für sich selbst löst. Stattdessen soll...

Danke für die schnelle Antwort. Ich glaube jetzt habe ich es verstanden. Ich wollte mit folgenden Satz: Wenn man zulässt, dass die Variante Änderungen an Variablen nur unvollständig beschreiben darf wie hier im Fall bei der FIFO queue Q , benötigt man weitere Voraussetzungen um die Terminierung zu b...

Danke für die Antworten. Mir ist klar geworden, wie die Terminierung des Algorithmus gezeigt werden kann. Mein Problem war die Annahme, dass die Variante als alleinige Voraussetzung genügen soll (neben den impliziten allgemein üblichen Annahmen und Definitionen), um die Terminierung zu beweisen: Var...

Das beantwortet meine Frage teilweise. Ich kann nachvollziehen, dass Änderungen an Variablen, die keinen Einfluss auf die Abbruchbedingung haben, für den Korrektheitsbeweis unerheblich sind. Im gegebenen Fall ist die Abbruchbedingung " Q = \emptyset ." Das heißt sie hängt von der Variable Q ab. In d...

Hallo, mir ist beim Lesen des Wiki-Eintrags zur Breitensuchen (Breadth-first search) aufgefallen, dass dort als Variante One node is removed from Q . gewählt wurde. Nun wird im Abschnitt "Induction step" beschrieben, was innerhalb einer Iteration passiert: Extract the first element v from Q . Append...