Commit 502c972e authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update tests

parent 1a62b6c8
......@@ -30,3 +30,6 @@ tmp/
tests/res/dtmc/**/*.jani
tests/res/mdp/**/*.jani
#Pytest Coverage
cov.xml
.coverage
......@@ -23,18 +23,18 @@ JANI2PINS requires the following libraries to work correctly.
### Python 3.8
Install at least Python 3.8 from : <https://www.python.org/>
Install at least Python 3.8 from <https://www.python.org/>
### LTSmin Toolset v3.0.2
Download and install the toolset from: <https://ltsmin.utwente.nl/>
Download and install the toolset from <https://ltsmin.utwente.nl/>
### pytest 5.4.3
Install the test libraries with
```shell
pip install pytest==5.4.3
pip install pytest==6.0.1
pip install pytest-cov==2.10.0
```
......@@ -59,35 +59,34 @@ pip install websockets==8.1
For testing purposes, you can download more jani-models from the [QCOMP Benchmark Set](http://qcomp.org/benchmarks/index.html) by executing the following shell script in the tests directory
```shell
cd JANI2PINS/tests/
sh downloadModels.sh
sh tests/downloadModels.sh
```
---
## Usage
In general, JANI2PINS creates the source code implementation of the dl-open API of LTSmin, according to its input in the [JANI]("http://www.jani-spec.org/") model format. Therefore, you have the following option to adjust the creation of the plugin implementation.
In general, JANI2PINS creates the source code implementation of the LTSmin's dl-open API, according to its input [jani-model]("http://www.jani-spec.org/"). Therefore, you have the following option to adjust the creation of the plugin implementation.
### --input PATH
Provide path to the input file, containing the jani-model
Provide the path to the input file containing the jani-model
### --output PATH
(default: CWD)
Provide path of location for creating PINS model implementation
Provide the path to PINS model implementation
### --ltsmin PATH
(default: "/usr/local/include/ltsmin/")
Location of LTSmin headers
Location of LTSmin header files
### --compile
Let JANI2PINS compile the plugin implementation after creation
Compile PINS model after creation in the filesystem
(Important: --ltsmin has to link to correct header location)
......@@ -97,11 +96,11 @@ Add values to uninitialized constants in jani-model, e.g. --experiment "C=42, D=
### --real2int
Cast real variables in jani-model to integer (Warning: Can produce wrong models)
Cast real variables in jani-model to integer (Warning: Can break jani-models)
### --disableCheck
Disable time consuming jani-model syntax check
Disable time-consuming jani-model syntax check
---
......@@ -111,15 +110,15 @@ Additionally, the JANI specification defines a WebSocket network protocol.
### --server
Run JANI2PINS as server, implementing interactive protocol
Run JANI2PINS as server implementation of the interactive protocol
(Important: --ltsmin has to link to correct header location)
(Important: --ltsmin has to link to correct header location)
### --address ADDRESS
(default: "localhost:15291")
Adjust web address of server
Adjust the web address of the server
---
......
def transientVariablesOf(automaton: dict) -> dict:
"""
Function Description:
Get updated values of transient variables
Function Parameters:
automaton : dict
automaton object of jani-model
"""
transientsByLocation = {}
for location in automaton["locations"]:
if "transient-values" in location:
name = location["name"]
transientsByLocation[name] = {}
for update in location["transient-values"]:
identifier = update["ref"]
transientsByLocation[name][identifier] = update["value"]
return transientsByLocation
def initialValueOf(variable: dict) -> int:
"""
Function Description:
......@@ -50,20 +30,3 @@ def variablesOf(automaton: dict) -> set:
identifier = variable["name"]
variableByIdentifier[identifier] = variable
return variableByIdentifier
def transientValuesOf(location: str, transientVariables: dict) -> dict:
"""
Function Description:
Get values for transient variables at location in automaton
Function Parameters:
location : str
location identifier in jani-model automaton
transientVariables: dict
transient variables of jani-model
"""
transientValues = dict()
if location in transientVariables:
transientValues = transientVariables[location]
return transientValues
......@@ -13,28 +13,23 @@ indent = 4
def nextStateFunctionsOf(pinsModel: Model) -> str:
modelGuards = pinsModel.getGuards()
stateVector = pinsModel.getStateVector()
modelLocations = pinsModel.getLocations()
locations = pinsModel.getLocations()
functions = createFunctionImplementationString(pinsModel.getFunctions())
constants = "\n".join(["// Model Constants"] + pinsModel.getConstants())
nextStatesLong = createNextStatesString(pinsModel, StateVectorMode.LONG)
nextStatesR2W = createNextStatesString(pinsModel, StateVectorMode.R2W)
actionsR2W = createActionsString(pinsModel, StateVectorMode.R2W)
guardsLong = modelGuards.evaluationCode(
stateVector, modelLocations, StateVectorMode.LONG
)
guardsLong = (
createTransientDeclaration(pinsModel, StateVectorMode.LONG, False) + guardsLong
)
guardsShort = modelGuards.evaluationCode(
stateVector, modelLocations, StateVectorMode.SHORT
guardsLong = createTransientDeclaration(pinsModel, StateVectorMode.LONG, False)
guardsLong += modelGuards.evaluationCode(
stateVector, locations, StateVectorMode.LONG
)
guardsShort = (
createTransientDeclaration(pinsModel, StateVectorMode.SHORT, False)
+ guardsShort
guardsShort = createTransientDeclaration(pinsModel, StateVectorMode.SHORT, False)
guardsShort += modelGuards.evaluationCode(
stateVector, locations, StateVectorMode.SHORT
)
labelEvaluationLong = ("\n" + indent * " ").join(guardsLong)
labelEvaluationShort = ("\n" + indent * " ").join(guardsShort)
initialStateVector = getInitialStateVectorString(stateVector, modelLocations)
initialStateVector = getInitialStateVectorString(stateVector, locations)
code = resources.read_text(placeholder, "nextStatesFunctions.placeholder")
code = code.format(
constants=constants,
......
......@@ -5,7 +5,7 @@ import src.pins.modules.constants as constants
import src.utilities.parser.expression.toRename as rename
from src.jani.functions import functionsOf
from src.jani.validation import isSupported, supportedVariable
from src.jani.variables import initialValueOf, transientValuesOf, transientVariablesOf
from src.jani.variables import initialValueOf
from src.pins.modules.actions import Actions
from src.pins.modules.guards import ModelGuards
from src.pins.modules.locations import Locations
......
def infixMerge(expressions: list, op: str) -> dict:
"""
Function Description:
Link expressions with operator together
Function Parameters:
expressions: list
Expressions, which will be merged together
op: str
Operator, which will link expressions together
"""
mergedExpression = expressions[0] if expressions else []
for expression_idx in range(1, len(expressions)):
mergedExpression = {
"left": expressions[expression_idx],
"op": op,
"right": mergedExpression,
}
return mergedExpression
def createExperiments(experimentValues: str) -> dict:
"""
Function Description:
......
#QCOMP
##DTMC
wget http://qcomp.org/benchmarks/dtmc/brp/brp.jani -O res/dtmc/brp/brp.jani
wget http://qcomp.org/benchmarks/dtmc/coupon/coupon.5-2.jani -O res/dtmc/coupon/coupon.5-2.jani
wget http://qcomp.org/benchmarks/dtmc/leader_sync/leader_sync.3-2.jani -O res/dtmc/leader_sync/leader_sync.3-2.jani
wget http://qcomp.org/benchmarks/dtmc/egl/egl.jani -O res/dtmc/egl/egl.v1.jani
wget http://qcomp.org/benchmarks/dtmc/brp/brp.jani -O tests/resdtmc/brp/brp.jani
wget http://qcomp.org/benchmarks/dtmc/coupon/coupon.5-2.jani -O tests/resdtmc/coupon/coupon.5-2.jani
wget http://qcomp.org/benchmarks/dtmc/leader_sync/leader_sync.3-2.jani -O tests/resdtmc/leader_sync/leader_sync.3-2.jani
wget http://qcomp.org/benchmarks/dtmc/egl/egl.jani -O tests/resdtmc/egl/egl.v1.jani
##MDP
wget http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani -O res/mdp/beb/beb.3-4.jani
wget http://qcomp.org/benchmarks/mdp/consensus/consensus.2.jani -O res/mdp/consensus/consensus.2.v1.jani
wget http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani -O res/mdp/csma/csma.2-2.v1.jani
wget http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani -O res/mdp/elevators/elevators.a-3-3.v1.jani
wget http://qcomp.org/benchmarks/mdp/rectangle-tireworld/rectangle-tireworld.5.jani -O res/mdp/rectangle-tireworld/rectangle-tireworld.5.v1.jani
wget http://qcomp.org/benchmarks/mdp/tireworld/tireworld.17.jani -O res/mdp/tireworld/tireworld.17.v1.jani
wget http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O res/mdp/wlan/wlan.0.v1.jani
\ No newline at end of file
wget http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani -O tests/resmdp/beb/beb.3-4.jani
wget http://qcomp.org/benchmarks/mdp/consensus/consensus.2.jani -O tests/resmdp/consensus/consensus.2.v1.jani
wget http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani -O tests/resmdp/csma/csma.2-2.v1.jani
wget http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani -O tests/resmdp/elevators/elevators.a-3-3.v1.jani
wget http://qcomp.org/benchmarks/mdp/rectangle-tireworld/rectangle-tireworld.5.jani -O tests/resmdp/rectangle-tireworld/rectangle-tireworld.5.v1.jani
wget http://qcomp.org/benchmarks/mdp/tireworld/tireworld.17.jani -O tests/resmdp/tireworld/tireworld.17.v1.jani
wget http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O tests/resmdp/wlan/wlan.0.v1.jani
\ No newline at end of file
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 2
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0},(int[]){1}};
int transitionGuardsSizes[GROUPAMOUNT] = {1,1};
guard_t **guard_info = malloc(GROUPAMOUNT * sizeof(guard_t *));
for (int i = 0; i < GROUPAMOUNT; i++)
{
guard_info[i] = malloc(sizeof(int[transitionGuardsSizes[i] + 1]));
memcpy(guard_info[i]->guard, transitionGuards[i], transitionGuardsSizes[i] * sizeof(int));
guard_info[i]->count = transitionGuardsSizes[i];
}
return guard_info;
}
#include <jani2pinsPlugin.h>
// Name of the PINS plugin
char pins_plugin_name[] = "jani2pins";
// Compute the remainder of Euclidean division
int remEuc(int x, int y){
int remainder = x % y;
if (remainder < 0){
return remainder + abs(y);
}
else{
return remainder;
}
}
// Compute the signum function
int sgn(int x){
if (x>0){
return 1;
}
if (x<0){
return -1;
}
return 0;
}
// Evaluate all state labels or guard
static void stateLabelsGroup(model_t model, sl_group_enum_t group, int *sourceStateVector, int *stateVectorLabels) {
if (group == GB_SL_GUARDS) {
for (int i = 0; i < guardAmount(); i++) {
stateVectorLabels[i] = stateVectorLabelLong(model, i, sourceStateVector);
}
}
if (group == GB_SL_ALL) {
for (int i = 0; i < labelAmount(); i++) {
stateVectorLabels[i] = stateVectorLabelLong(model, i, sourceStateVector);
}
}
}
// Initialise LTSmin Model
void pins_model_init(model_t model) {
// Initialise pins model
initModel(model);
// Set initial state
GBsetInitialState(model, initialStateVector());
//Set pointer to next-state function
GBsetNextStateLong(model, (next_method_grey_t)nextStateLong);
GBsetNextStateShortR2W(model, (next_method_grey_t)nextStateR2W);
GBsetActionsShortR2W(model, (next_method_grey_t)actionsR2W);
//Set pointer to label evaluation function
GBsetStateLabelLong(model, (get_label_method_t)stateVectorLabelLong);
GBsetStateLabelShort(model, (get_label_method_t)stateVectorLabelShort);
// Add new implementation
GBsetStateLabelsGroup(model, stateLabelsGroup);
// Create dependent matrices
matrix_t *rm = malloc(sizeof(matrix_t));
matrix_t *wm = malloc(sizeof(matrix_t));
matrix_t *cm = malloc(sizeof(matrix_t));
matrix_t *lm = malloc(sizeof(matrix_t));
matrix_t *dna = malloc(sizeof(matrix_t));
matrix_t *nes = malloc(sizeof(matrix_t));
matrix_t *nds = malloc(sizeof(matrix_t));
matrix_t *mce = malloc(sizeof(matrix_t));
dm_create(rm, groupAmount(), stateVectorLength());
dm_create(wm, groupAmount(), stateVectorLength());
dm_create(cm, groupAmount(), stateVectorLength());
dm_create(lm, labelAmount(), stateVectorLength());
dm_create(dna, groupAmount(), groupAmount());
dm_create(nes, guardAmount(), groupAmount());
dm_create(nds, guardAmount(), groupAmount());
dm_create(mce, guardAmount(), guardAmount());
// Set read & write dependency matrices
for (int i = 0; i < groupAmount(); i++) {
for (int j = 0; j < stateVectorLength(); j++) {
if (readDependencies(i)[j]) {
dm_set(cm, i, j);
dm_set(rm, i, j);
}
if (writeDependencies(i)[j]) {
dm_set(cm, i, j);
dm_set(wm, i, j);
}
}
}
// Set label dependency matrix
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < stateVectorLength(); j++) {
if (labelDependencies(i)[j]) {
dm_set(lm, i, j);
}
}
}
// Set do-not-accord matrix
for (int i = 0; i < groupAmount(); i++) {
for (int j = 0; j < groupAmount(); j++) {
if (dnaGroup(i)[j]) {
dm_set(dna, i, j);
}
}
}
// Set necessary enabling set and necessary disabling set
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < groupAmount(); j++) {
if (necessaryEnabling(i)[j]) {
dm_set(nes, i, j);
}
if (necessaryDisabling(i)[j]) {
dm_set(nds, i, j);
}
}
}
// Set may-be-co-enabled matrix
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < labelAmount(); j++) {
if (maybeCoEnabled(i)[j]) {
dm_set(mce, i, j);
}
}
}
// Set pointer to dependency matrices
GBsetDMInfoRead(model, rm);
GBsetDMInfoMustWrite(model, wm);
GBsetDMInfo(model, cm);
GBsetStateLabelInfo(model, lm);
GBsetDoNotAccordInfo(model, dna);
GBsetGuardNESInfo(model, nes);
GBsetGuardNDSInfo(model, nds);
GBsetGuardCoEnabledInfo(model, mce);
// Create Label Mapping
sl_group_t *sl_group_all = malloc(labelAmount() * sizeof(sl_group_all));
sl_group_all->count = labelAmount();
for (int i = 0; i < labelAmount(); i++) {
sl_group_all->sl_idx[i] = i;
}
// Create Guard Mapping
sl_group_t *sl_group_guards = malloc(guardAmount() * sizeof(sl_group_guards));
sl_group_guards->count = guardAmount();
for (int i = 0; i < guardAmount(); i++) {
sl_group_guards->sl_idx[i] = i;
}
// Set pointer to label & guard mappings
GBsetStateLabelGroupInfo(model, GB_SL_ALL, sl_group_all);
GBsetStateLabelGroupInfo(model, GB_SL_GUARDS, sl_group_guards);
// Add Action guards
GBsetGuardsInfo(model, createTransitionGroupGuardInformation());
// Printing Guards in stdout
GBprintStateLabelGroupInfo(stdout, model);
}
\ No newline at end of file
#include <ltsmin/dlopen-api.h>
#include <ltsmin/lts-type.h>
#include <ltsmin/ltsmin-standard.h>
#include <ltsmin/pins-util.h>
#include <ltsmin/pins.h>
#include <math.h>
//
// model.c
//
// The amount of all defined groups
int groupAmount();
// The amount of all defined labels
int labelAmount();
// The amount of all defined guards
int guardAmount();
// The length of the whole state vector
int stateVectorLength();
// Initialise the PINS model
void initModel(model_t model);
// Implementation of calculating remainder of Euclidean division
int remEuc(int x, int y);
// Compute the signum function
int sgn(int x);
//
// next-states.c
//
// The initial state vector
int *initialStateVector();
// Successor function for PINS model using a LONG state vector.
int nextStateLong(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Successor function for PINS model using a R2W state vector.
int nextStateR2W(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Update function for PINS model using a R2W state vector.
int actionsR2W(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Label function for LONG state vector:
int stateVectorLabelLong(model_t model, int label, int *state_src);
// Label function for SHORT state vector:
int stateVectorLabelShort(model_t model, int label, int *state_src);
//
// dependencies.c
//
// Read dependencies to state vector
int *readDependencies(int group);
// Write Dependencies
int *writeDependencies(int group);
// Label Dependencies
int *labelDependencies(int label);
// Do not accord
int *dnaGroup(int group);
// Necessary Enabling
int *necessaryEnabling(int guard);
// Necessary Disabling
int *necessaryDisabling(int guard);
// Maybe co-enabled
int *maybeCoEnabled(int guard);
//
// guards.c
//
//Create Action Guards
guard_t **createTransitionGroupGuardInformation();
\ No newline at end of file
#include <jani2pinsPlugin.h>
// Read dependencies to state vector
int readMatrix[2][1] = {{1},{1}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[2][1] = {{1},{1}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[2][1] = {{1},{1}};
int *labelDependencies(int label){
return labelMatrix[label];
}
// Do-not-accord
int DNAMatrix[2][2] = {{1,1},{1,1}};
int *dnaGroup(int group){
return DNAMatrix[group];
}
// Necessary Enabling
int NESMatrix[2][2] = {{1,1},{1,1}};
int *necessaryEnabling(int guard){
return NESMatrix[guard];
}
// Necessary Disabling
int NDSMatrix[2][2] = {{1,1},{1,1}};
int *necessaryDisabling(int guard){
return NDSMatrix[guard];
}
// Maybe co-enabled
int MCEMatrix[2][2] = {{1,0},{0,1}};
int *maybeCoEnabled(int guard){
return MCEMatrix[guard];
}
\ No newline at end of file
#include <jani2pinsPlugin.h>
// The amount of all defined groups
int groupAmount(){
return 2;
}
// The amount of all defined labels
int labelAmount()
{
return 2;
}
// The amount of all defined guards
int guardAmount()
{
return 2;
}
// The length of the whole state vector
int stateVectorLength()
{
return 1;
}
// Initialise the PINS model
void initModel(model_t model)
{
// Create empty lts datastructure
lts_type_t lts = lts_type_create();
// Create slot types
int intSlot = lts_type_put_type(lts, "int", LTStypeSInt32, NULL);
int actionSlot = lts_type_put_type(lts, "action", LTStypeEnum, NULL);
int guardSlot = lts_type_put_type(lts, "guard", LTStypeBool, NULL);
int boolSlot = lts_type_put_type(lts, "bool", LTStypeBool, NULL);