-
Notifications
You must be signed in to change notification settings - Fork 34
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
Showing
46 changed files
with
5,558 additions
and
0 deletions.
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
74 changes: 74 additions & 0 deletions
74
api/src/main/java/net/automatalib/automaton/ra/Assignment.java
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,74 @@ | ||
/* | ||
* Copyright (C) 2014-2015 The LearnLib Contributors | ||
* This file is part of LearnLib, http://www.learnlib.de/. | ||
* | ||
* Licensed under the Apache License, Version 2.0 (the "License"); | ||
* you may not use this file except in compliance with the License. | ||
* You may obtain a copy of the License at | ||
* | ||
* http://www.apache.org/licenses/LICENSE-2.0 | ||
* | ||
* Unless required by applicable law or agreed to in writing, software | ||
* distributed under the License is distributed on an "AS IS" BASIS, | ||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
* See the License for the specific language governing permissions and | ||
* limitations under the License. | ||
*/ | ||
package net.automatalib.automaton.ra; | ||
|
||
import java.util.Map.Entry; | ||
|
||
import net.automatalib.data.Constants; | ||
import net.automatalib.data.ParValuation; | ||
import net.automatalib.data.SymbolicDataValue; | ||
import net.automatalib.data.SymbolicDataValue.Constant; | ||
import net.automatalib.data.SymbolicDataValue.Parameter; | ||
import net.automatalib.data.SymbolicDataValue.Register; | ||
import net.automatalib.data.VarMapping; | ||
import net.automatalib.data.VarValuation; | ||
|
||
/** | ||
* A parallel assignment for registers. | ||
* | ||
* @author falk | ||
*/ | ||
public class Assignment { | ||
|
||
private final VarMapping<Register, ? extends SymbolicDataValue> assignment; | ||
|
||
public Assignment(VarMapping<Register, ? extends SymbolicDataValue> assignment) { | ||
this.assignment = assignment; | ||
} | ||
|
||
public VarValuation compute(VarValuation registers, ParValuation parameters, Constants consts) { | ||
VarValuation val = new VarValuation(registers); | ||
for (Entry<Register, ? extends SymbolicDataValue> e : assignment) { | ||
SymbolicDataValue valp = e.getValue(); | ||
if (valp.isRegister()) { | ||
val.put(e.getKey(), registers.get( (Register) valp)); | ||
} | ||
else if (valp.isParameter()) { | ||
val.put(e.getKey(), parameters.get( (Parameter) valp)); | ||
} | ||
//TODO: check if we want to copy constant values into vars | ||
else if (valp.isConstant()) { | ||
val.put(e.getKey(), consts.get( (Constant) valp)); | ||
} | ||
else { | ||
throw new IllegalStateException("Illegal assignment: " + | ||
e.getKey() + " := " + valp); | ||
} | ||
} | ||
return val; | ||
} | ||
|
||
@Override | ||
public String toString() { | ||
return assignment.toString(":="); | ||
} | ||
|
||
public VarMapping<Register, ? extends SymbolicDataValue> getAssignment() { | ||
return assignment; | ||
} | ||
|
||
} |
38 changes: 38 additions & 0 deletions
38
api/src/main/java/net/automatalib/automaton/ra/GuardExpression.java
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,38 @@ | ||
/* | ||
* Copyright (C) 2014-2015 The LearnLib Contributors | ||
* This file is part of LearnLib, http://www.learnlib.de/. | ||
* | ||
* Licensed under the Apache License, Version 2.0 (the "License"); | ||
* you may not use this file except in compliance with the License. | ||
* You may obtain a copy of the License at | ||
* | ||
* http://www.apache.org/licenses/LICENSE-2.0 | ||
* | ||
* Unless required by applicable law or agreed to in writing, software | ||
* distributed under the License is distributed on an "AS IS" BASIS, | ||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
* See the License for the specific language governing permissions and | ||
* limitations under the License. | ||
*/ | ||
package net.automatalib.automaton.ra; | ||
|
||
import java.util.Set; | ||
|
||
import net.automatalib.data.DataValue; | ||
import net.automatalib.data.Mapping; | ||
import net.automatalib.data.SymbolicDataValue; | ||
import net.automatalib.data.VarMapping; | ||
|
||
/** | ||
* | ||
* @author falk | ||
* | ||
*/ | ||
public interface GuardExpression { | ||
|
||
GuardExpression relabel(VarMapping relabelling); | ||
|
||
boolean isSatisfied(Mapping<SymbolicDataValue, DataValue<?>> val); | ||
|
||
Set<SymbolicDataValue> getSymbolicDataValues(); | ||
} |
29 changes: 29 additions & 0 deletions
29
api/src/main/java/net/automatalib/automaton/ra/MutableRegisterAutomaton.java
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,29 @@ | ||
/* | ||
* Copyright (C) 2014-2015 The LearnLib Contributors | ||
* This file is part of LearnLib, http://www.learnlib.de/. | ||
* | ||
* Licensed under the Apache License, Version 2.0 (the "License"); | ||
* you may not use this file except in compliance with the License. | ||
* You may obtain a copy of the License at | ||
* | ||
* http://www.apache.org/licenses/LICENSE-2.0 | ||
* | ||
* Unless required by applicable law or agreed to in writing, software | ||
* distributed under the License is distributed on an "AS IS" BASIS, | ||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
* See the License for the specific language governing permissions and | ||
* limitations under the License. | ||
*/ | ||
package net.automatalib.automaton.ra; | ||
|
||
import net.automatalib.automaton.MutableDeterministic; | ||
import net.automatalib.symbol.ParameterizedSymbol; | ||
|
||
/** | ||
* Mutable Register Automaton. | ||
* | ||
* @author falk | ||
*/ | ||
public interface MutableRegisterAutomaton extends RegisterAutomaton, MutableDeterministic<RALocation, ParameterizedSymbol, Transition, Boolean, Void> { | ||
|
||
} |
112 changes: 112 additions & 0 deletions
112
api/src/main/java/net/automatalib/automaton/ra/RALocation.java
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,112 @@ | ||
/* | ||
* Copyright (C) 2014-2015 The LearnLib Contributors | ||
* This file is part of LearnLib, http://www.learnlib.de/. | ||
* | ||
* Licensed under the Apache License, Version 2.0 (the "License"); | ||
* you may not use this file except in compliance with the License. | ||
* You may obtain a copy of the License at | ||
* | ||
* http://www.apache.org/licenses/LICENSE-2.0 | ||
* | ||
* Unless required by applicable law or agreed to in writing, software | ||
* distributed under the License is distributed on an "AS IS" BASIS, | ||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
* See the License for the specific language governing permissions and | ||
* limitations under the License. | ||
*/ | ||
package net.automatalib.automaton.ra; | ||
|
||
import static java.util.Collections.emptySet; | ||
|
||
import java.util.ArrayList; | ||
import java.util.Collection; | ||
import java.util.LinkedHashMap; | ||
import java.util.Map; | ||
|
||
import net.automatalib.symbol.ParameterizedSymbol; | ||
|
||
/** | ||
* | ||
* @author falk | ||
*/ | ||
public class RALocation { | ||
|
||
private final int id; | ||
|
||
private boolean accepting; | ||
|
||
private final Map<ParameterizedSymbol, Collection<Transition>> out = new LinkedHashMap<>(); | ||
|
||
public RALocation(int id, boolean accepting) { | ||
this.id = id; | ||
this.accepting = accepting; | ||
} | ||
|
||
public RALocation(int id) { | ||
this(id, true); | ||
} | ||
|
||
public Collection<Transition> getOut(ParameterizedSymbol ps) { | ||
return out.getOrDefault(ps, emptySet()); | ||
} | ||
|
||
public Collection<Transition> getOut() { | ||
ArrayList<Transition> ret = new ArrayList<>(); | ||
for (Collection<Transition> col : out.values()) { | ||
ret.addAll(col); | ||
} | ||
return ret; | ||
} | ||
|
||
public void addOut(Transition t) { | ||
Collection<Transition> c = out.get(t.getLabel()); | ||
if (c == null) { | ||
c = new ArrayList<>(); | ||
out.put(t.getLabel(), c); | ||
} | ||
c.add(t); | ||
} | ||
|
||
public void clear() { | ||
this.out.clear(); | ||
} | ||
|
||
@Override | ||
public int hashCode() { | ||
int hash = 7; | ||
hash = 23 * hash + this.id; | ||
return hash; | ||
} | ||
|
||
@Override | ||
public boolean equals(Object obj) { | ||
if (obj == null) { | ||
return false; | ||
} | ||
if (getClass() != obj.getClass()) { | ||
return false; | ||
} | ||
final RALocation other = (RALocation) obj; | ||
if (this.id != other.id) { | ||
return false; | ||
} | ||
return true; | ||
} | ||
|
||
@Override | ||
public String toString() { | ||
return "l" + id + " (" + (this.accepting ? "+" : "-") +")"; | ||
} | ||
|
||
public String getName() { | ||
return "l" + id; | ||
} | ||
|
||
public boolean isAccepting() { | ||
return this.accepting; | ||
} | ||
|
||
public void setAccepting(boolean accepting) { | ||
this.accepting = accepting; | ||
} | ||
} |
48 changes: 48 additions & 0 deletions
48
api/src/main/java/net/automatalib/automaton/ra/RegisterAutomaton.java
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,48 @@ | ||
/* | ||
* Copyright (C) 2014-2015 The LearnLib Contributors | ||
* This file is part of LearnLib, http://www.learnlib.de/. | ||
* | ||
* Licensed under the Apache License, Version 2.0 (the "License"); | ||
* you may not use this file except in compliance with the License. | ||
* You may obtain a copy of the License at | ||
* | ||
* http://www.apache.org/licenses/LICENSE-2.0 | ||
* | ||
* Unless required by applicable law or agreed to in writing, software | ||
* distributed under the License is distributed on an "AS IS" BASIS, | ||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
* See the License for the specific language governing permissions and | ||
* limitations under the License. | ||
*/ | ||
package net.automatalib.automaton.ra; | ||
|
||
import java.util.Collection; | ||
import java.util.List; | ||
|
||
import net.automatalib.automaton.DeterministicAutomaton; | ||
import net.automatalib.data.SymbolicDataValue.Register; | ||
import net.automatalib.data.VarValuation; | ||
import net.automatalib.symbol.PSymbolInstance; | ||
import net.automatalib.symbol.ParameterizedSymbol; | ||
import net.automatalib.word.Word; | ||
|
||
/** | ||
* | ||
* @author falk | ||
*/ | ||
public interface RegisterAutomaton extends DeterministicAutomaton<RALocation, ParameterizedSymbol, Transition> { | ||
|
||
boolean accepts(Word<PSymbolInstance> dw); | ||
|
||
RALocation getLocation(Word<PSymbolInstance> dw); | ||
|
||
VarValuation getInitialRegisters(); | ||
|
||
List<Transition> getTransitions(); | ||
|
||
List<Transition> getInputTransitions(); | ||
|
||
Collection<RALocation> getInputStates(); | ||
|
||
Collection<Register> getRegisters(); | ||
} |
Oops, something went wrong.