-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
db3b316
commit e2511a1
Showing
17 changed files
with
299 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
import java.util.List; | ||
|
||
@Getter | ||
public class Automaton { | ||
private State startState; | ||
private List<Region> regions; | ||
private List<State> states; | ||
private List<Edge> edges; | ||
|
||
public Automaton(State startState) { | ||
//TODO stub | ||
this.startState = startState; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class Condition { | ||
private String condition; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class Contract { | ||
private Condition preCondition; | ||
private Condition postCondition; | ||
|
||
public Contract(Condition preCondition, Condition postCondition) { | ||
//TODO stub | ||
this.preCondition = preCondition; | ||
this.postCondition = postCondition; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class DeleteElementVisitor implements ElementVisitor { | ||
private System parentSystem; | ||
@Override | ||
public void visit(State state) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class Edge implements Element { | ||
private Contract contract; | ||
private Kind kind; | ||
private int priority; | ||
|
||
public Edge(Contract contract, Kind kind, int priority) { | ||
//TODO stub | ||
this.contract = contract; | ||
this.kind = kind; | ||
this.priority = priority; | ||
} | ||
@Override | ||
public void accept(ElementVisitor visitor) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,5 @@ | ||
package org.gecko.model; | ||
|
||
public class Element { | ||
public interface Element { | ||
public void accept(ElementVisitor visitor); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package org.gecko.model; | ||
|
||
public interface ElementVisitor { | ||
public void visit(State state); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class GeckoModel { | ||
private System root; | ||
public ModelFactory getModelFactory() { | ||
//TODO stub | ||
return new ModelFactory(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
package org.gecko.model; | ||
|
||
public enum Kind { | ||
HIT, | ||
MISS, | ||
FAIL | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
package org.gecko.model; | ||
|
||
public class ModelFactory { | ||
public State createState(Automaton automaton) { | ||
//TODO stub | ||
return new State(); | ||
} | ||
|
||
public Edge createEdge(Automaton automaton, Contract contract, Kind kind, int priority) { | ||
//TODO stub | ||
return new Edge(contract, kind, priority); | ||
} | ||
|
||
public System createSystem(System parentSystem) { | ||
//TODO stub | ||
return new System(); | ||
} | ||
|
||
public Variable createVariable(System system) { | ||
//TODO stub | ||
return new Variable(); | ||
} | ||
|
||
public SystemConnection createSystemConnection(System system, Variable source, Variable destination) { | ||
//TODO stub | ||
return new SystemConnection(source, destination); | ||
} | ||
|
||
public Contract createContract(State state, Condition preCondition, Condition postCondition) { | ||
//TODO stub | ||
return new Contract(preCondition, postCondition); | ||
} | ||
|
||
public Region createRegion(Automaton automaton, Condition invariant, Contract preAndPostCondition) { | ||
//TODO stub | ||
return new Region(invariant, preAndPostCondition); | ||
} | ||
|
||
public Automaton createAutomaton(System system, State startState) { | ||
//TODO stub | ||
return new Automaton(startState); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
import java.util.List; | ||
|
||
public class Region implements Renamable, Element { | ||
@Getter | ||
private Condition invariant; | ||
private Contract preAndPostCondition; | ||
@Getter | ||
private List<State> states; | ||
|
||
public Region(Condition invariant, Contract preAndPostCondition) { | ||
this.invariant = invariant; | ||
this.preAndPostCondition = preAndPostCondition; | ||
} | ||
@Override | ||
public void accept(ElementVisitor visitor) { | ||
//TODO stub | ||
} | ||
|
||
@Override | ||
public String getName() { | ||
//TODO stub | ||
return null; | ||
} | ||
|
||
@Override | ||
public void setName(String name) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
package org.gecko.model; | ||
|
||
public interface Renamable { | ||
public String getName(); | ||
public void setName(String name); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
import java.util.List; | ||
|
||
@Getter | ||
public class State implements Renamable, Element { | ||
private List<Contract> contracts; | ||
|
||
@Override | ||
public void accept(ElementVisitor visitor) { | ||
//TODO stub | ||
} | ||
|
||
@Override | ||
public String getName() { | ||
//TODO stub | ||
return null; | ||
} | ||
|
||
@Override | ||
public void setName(String name) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
import lombok.Setter; | ||
|
||
import java.util.List; | ||
|
||
public class System implements Renamable, Element { | ||
@Getter | ||
private System parent; | ||
@Getter | ||
private String code; | ||
@Getter | ||
private Automaton automaton; | ||
@Getter | ||
private List<System> children; | ||
private List<SystemConnection> connections; | ||
private List<Variable> variables; | ||
|
||
public void addChild(System child) { | ||
//TODO stub | ||
children.add(child); | ||
} | ||
|
||
@Override | ||
public void accept(ElementVisitor visitor) { | ||
//TODO stub | ||
} | ||
|
||
@Override | ||
public String getName() { | ||
//TODO stub | ||
return null; | ||
} | ||
|
||
@Override | ||
public void setName(String name) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class SystemConnection implements Element { | ||
private Variable source; | ||
private Variable destination; | ||
|
||
public SystemConnection(Variable source, Variable destination) { | ||
this.source = source; | ||
this.destination = destination; | ||
} | ||
@Override | ||
public void accept(ElementVisitor visitor) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
package org.gecko.model; | ||
|
||
import lombok.Getter; | ||
|
||
@Getter | ||
public class Variable implements Renamable, Element { | ||
private Visibility visibility; | ||
private String name; | ||
private String type; | ||
|
||
@Override | ||
public void accept(ElementVisitor visitor) { | ||
//TODO stub | ||
} | ||
|
||
@Override | ||
public String getName() { | ||
//TODO stub | ||
return null; | ||
} | ||
|
||
@Override | ||
public void setName(String name) { | ||
//TODO stub | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
package org.gecko.model; | ||
|
||
public enum Visibility { | ||
INPUT, | ||
OUTPUT, | ||
STATE | ||
} |