Commit b46eef06 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update tests

parent bae4c450
......@@ -13,4 +13,6 @@ wget -4 http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani -O tests/res/mdp/csma
wget -4 http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani -O tests/res/mdp/elevators/elevators.a-3-3.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/rectangle-tireworld/rectangle-tireworld.5.jani -O tests/res/mdp/rectangle-tireworld/rectangle-tireworld.5.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/tireworld/tireworld.17.jani -O tests/res/mdp/tireworld/tireworld.17.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O tests/res/mdp/wlan/wlan.0.v1.jani
\ No newline at end of file
wget -4 http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O tests/res/mdp/wlan/wlan.0.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/pnueli-zuck/pnueli-zuck.3.jani -O tests/res/mdp/pnueli-zuck/pnueli-zuck.3.jani
wget -4 http://qcomp.org/benchmarks/mdp/triangle-tireworld/triangle-tireworld.9.jani -O tests/res/mdp/triangle-tireworld/triangle-tireworld.9.jani
\ No newline at end of file
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 75
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0},(int[]){1},(int[]){2},(int[]){3},(int[]){4},(int[]){0},(int[]){5},(int[]){6},(int[]){7},(int[]){8},(int[]){8},(int[]){9},(int[]){10},(int[]){11},(int[]){12},(int[]){13},(int[]){14},(int[]){15},(int[]){16},(int[]){17},(int[]){17},(int[]){18},(int[]){19},(int[]){20},(int[]){21},(int[]){22},(int[]){23},(int[]){24},(int[]){25},(int[]){26},(int[]){22},(int[]){27},(int[]){28},(int[]){29},(int[]){30},(int[]){30},(int[]){31},(int[]){32},(int[]){33},(int[]){34},(int[]){35},(int[]){36},(int[]){37},(int[]){38},(int[]){39},(int[]){39},(int[]){40},(int[]){41},(int[]){42},(int[]){43},(int[]){44},(int[]){45},(int[]){46},(int[]){47},(int[]){48},(int[]){44},(int[]){49},(int[]){50},(int[]){51},(int[]){52},(int[]){52},(int[]){53},(int[]){54},(int[]){55},(int[]){56},(int[]){57},(int[]){58},(int[]){59},(int[]){60},(int[]){61},(int[]){61},(int[]){62},(int[]){63},(int[]){64},(int[]){65}};
int transitionGuardsSizes[GROUPAMOUNT] = {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,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
This diff is collapsed.
#include <jani2pinsPlugin.h>
// The amount of all defined groups
int groupAmount(){
return 75;
}
// The amount of all defined labels
int labelAmount()
{
return 66;
}
// The amount of all defined guards
int guardAmount()
{
return 66;
}
// The length of the whole state vector
int stateVectorLength()
{
return 6;
}
// 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);
// Define action edges
lts_type_set_edge_label_count(lts, 1);
lts_type_set_edge_label_name(lts, 0, "action");
lts_type_set_edge_label_type(lts, 0, "action");
lts_type_set_edge_label_typeno(lts, 0, actionSlot);
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "process0_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "process1_instance_0");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "process2_instance_0");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "p0");
lts_type_set_state_typeno(lts, 3, intSlot);
lts_type_set_state_name(lts, 4, "p1");
lts_type_set_state_typeno(lts, 4, intSlot);
lts_type_set_state_name(lts, 5, "p2");
lts_type_set_state_typeno(lts, 5, intSlot);
// Define StateLabels
lts_type_set_state_label_count(lts, labelAmount());
lts_type_set_state_label_name(lts, 0, "g_0");
lts_type_set_state_label_typeno(lts, 0, guardSlot);
lts_type_set_state_label_name(lts, 1, "g_1");
lts_type_set_state_label_typeno(lts, 1, guardSlot);
lts_type_set_state_label_name(lts, 2, "g_2");
lts_type_set_state_label_typeno(lts, 2, guardSlot);
lts_type_set_state_label_name(lts, 3, "g_3");
lts_type_set_state_label_typeno(lts, 3, guardSlot);
lts_type_set_state_label_name(lts, 4, "g_4");
lts_type_set_state_label_typeno(lts, 4, guardSlot);
lts_type_set_state_label_name(lts, 5, "g_5");
lts_type_set_state_label_typeno(lts, 5, guardSlot);
lts_type_set_state_label_name(lts, 6, "g_6");
lts_type_set_state_label_typeno(lts, 6, guardSlot);
lts_type_set_state_label_name(lts, 7, "g_7");
lts_type_set_state_label_typeno(lts, 7, guardSlot);
lts_type_set_state_label_name(lts, 8, "g_8");
lts_type_set_state_label_typeno(lts, 8, guardSlot);
lts_type_set_state_label_name(lts, 9, "g_9");
lts_type_set_state_label_typeno(lts, 9, guardSlot);
lts_type_set_state_label_name(lts, 10, "g_10");
lts_type_set_state_label_typeno(lts, 10, guardSlot);
lts_type_set_state_label_name(lts, 11, "g_11");
lts_type_set_state_label_typeno(lts, 11, guardSlot);
lts_type_set_state_label_name(lts, 12, "g_12");
lts_type_set_state_label_typeno(lts, 12, guardSlot);
lts_type_set_state_label_name(lts, 13, "g_13");
lts_type_set_state_label_typeno(lts, 13, guardSlot);
lts_type_set_state_label_name(lts, 14, "g_14");
lts_type_set_state_label_typeno(lts, 14, guardSlot);
lts_type_set_state_label_name(lts, 15, "g_15");
lts_type_set_state_label_typeno(lts, 15, guardSlot);
lts_type_set_state_label_name(lts, 16, "g_16");
lts_type_set_state_label_typeno(lts, 16, guardSlot);
lts_type_set_state_label_name(lts, 17, "g_17");
lts_type_set_state_label_typeno(lts, 17, guardSlot);
lts_type_set_state_label_name(lts, 18, "g_18");
lts_type_set_state_label_typeno(lts, 18, guardSlot);
lts_type_set_state_label_name(lts, 19, "g_19");
lts_type_set_state_label_typeno(lts, 19, guardSlot);
lts_type_set_state_label_name(lts, 20, "g_20");
lts_type_set_state_label_typeno(lts, 20, guardSlot);
lts_type_set_state_label_name(lts, 21, "g_21");
lts_type_set_state_label_typeno(lts, 21, guardSlot);
lts_type_set_state_label_name(lts, 22, "g_22");
lts_type_set_state_label_typeno(lts, 22, guardSlot);
lts_type_set_state_label_name(lts, 23, "g_23");
lts_type_set_state_label_typeno(lts, 23, guardSlot);
lts_type_set_state_label_name(lts, 24, "g_24");
lts_type_set_state_label_typeno(lts, 24, guardSlot);
lts_type_set_state_label_name(lts, 25, "g_25");
lts_type_set_state_label_typeno(lts, 25, guardSlot);
lts_type_set_state_label_name(lts, 26, "g_26");
lts_type_set_state_label_typeno(lts, 26, guardSlot);
lts_type_set_state_label_name(lts, 27, "g_27");
lts_type_set_state_label_typeno(lts, 27, guardSlot);
lts_type_set_state_label_name(lts, 28, "g_28");
lts_type_set_state_label_typeno(lts, 28, guardSlot);
lts_type_set_state_label_name(lts, 29, "g_29");
lts_type_set_state_label_typeno(lts, 29, guardSlot);
lts_type_set_state_label_name(lts, 30, "g_30");
lts_type_set_state_label_typeno(lts, 30, guardSlot);
lts_type_set_state_label_name(lts, 31, "g_31");
lts_type_set_state_label_typeno(lts, 31, guardSlot);
lts_type_set_state_label_name(lts, 32, "g_32");
lts_type_set_state_label_typeno(lts, 32, guardSlot);
lts_type_set_state_label_name(lts, 33, "g_33");
lts_type_set_state_label_typeno(lts, 33, guardSlot);
lts_type_set_state_label_name(lts, 34, "g_34");
lts_type_set_state_label_typeno(lts, 34, guardSlot);
lts_type_set_state_label_name(lts, 35, "g_35");
lts_type_set_state_label_typeno(lts, 35, guardSlot);
lts_type_set_state_label_name(lts, 36, "g_36");
lts_type_set_state_label_typeno(lts, 36, guardSlot);
lts_type_set_state_label_name(lts, 37, "g_37");
lts_type_set_state_label_typeno(lts, 37, guardSlot);
lts_type_set_state_label_name(lts, 38, "g_38");
lts_type_set_state_label_typeno(lts, 38, guardSlot);
lts_type_set_state_label_name(lts, 39, "g_39");
lts_type_set_state_label_typeno(lts, 39, guardSlot);
lts_type_set_state_label_name(lts, 40, "g_40");
lts_type_set_state_label_typeno(lts, 40, guardSlot);
lts_type_set_state_label_name(lts, 41, "g_41");
lts_type_set_state_label_typeno(lts, 41, guardSlot);
lts_type_set_state_label_name(lts, 42, "g_42");
lts_type_set_state_label_typeno(lts, 42, guardSlot);
lts_type_set_state_label_name(lts, 43, "g_43");
lts_type_set_state_label_typeno(lts, 43, guardSlot);
lts_type_set_state_label_name(lts, 44, "g_44");
lts_type_set_state_label_typeno(lts, 44, guardSlot);
lts_type_set_state_label_name(lts, 45, "g_45");
lts_type_set_state_label_typeno(lts, 45, guardSlot);
lts_type_set_state_label_name(lts, 46, "g_46");
lts_type_set_state_label_typeno(lts, 46, guardSlot);
lts_type_set_state_label_name(lts, 47, "g_47");
lts_type_set_state_label_typeno(lts, 47, guardSlot);
lts_type_set_state_label_name(lts, 48, "g_48");
lts_type_set_state_label_typeno(lts, 48, guardSlot);
lts_type_set_state_label_name(lts, 49, "g_49");
lts_type_set_state_label_typeno(lts, 49, guardSlot);
lts_type_set_state_label_name(lts, 50, "g_50");
lts_type_set_state_label_typeno(lts, 50, guardSlot);
lts_type_set_state_label_name(lts, 51, "g_51");
lts_type_set_state_label_typeno(lts, 51, guardSlot);
lts_type_set_state_label_name(lts, 52, "g_52");
lts_type_set_state_label_typeno(lts, 52, guardSlot);
lts_type_set_state_label_name(lts, 53, "g_53");
lts_type_set_state_label_typeno(lts, 53, guardSlot);
lts_type_set_state_label_name(lts, 54, "g_54");
lts_type_set_state_label_typeno(lts, 54, guardSlot);
lts_type_set_state_label_name(lts, 55, "g_55");
lts_type_set_state_label_typeno(lts, 55, guardSlot);
lts_type_set_state_label_name(lts, 56, "g_56");
lts_type_set_state_label_typeno(lts, 56, guardSlot);
lts_type_set_state_label_name(lts, 57, "g_57");
lts_type_set_state_label_typeno(lts, 57, guardSlot);
lts_type_set_state_label_name(lts, 58, "g_58");
lts_type_set_state_label_typeno(lts, 58, guardSlot);
lts_type_set_state_label_name(lts, 59, "g_59");
lts_type_set_state_label_typeno(lts, 59, guardSlot);
lts_type_set_state_label_name(lts, 60, "g_60");
lts_type_set_state_label_typeno(lts, 60, guardSlot);
lts_type_set_state_label_name(lts, 61, "g_61");
lts_type_set_state_label_typeno(lts, 61, guardSlot);
lts_type_set_state_label_name(lts, 62, "g_62");
lts_type_set_state_label_typeno(lts, 62, guardSlot);
lts_type_set_state_label_name(lts, 63, "g_63");
lts_type_set_state_label_typeno(lts, 63, guardSlot);
lts_type_set_state_label_name(lts, 64, "g_64");
lts_type_set_state_label_typeno(lts, 64, guardSlot);
lts_type_set_state_label_name(lts, 65, "g_65");
lts_type_set_state_label_typeno(lts, 65, guardSlot);
// Validate lts datastructure
lts_type_validate(lts);
// Add lts to pins model
GBsetLTStype(model, lts);
// Add names to action groups
pins_chunk_put(model, actionSlot, chunk_str("tau"));
}
This source diff could not be displayed because it is too large. You can view the blob instead.
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 20
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0},(int[]){1},(int[]){2},(int[]){3},(int[]){4},(int[]){4},(int[]){4},(int[]){4},(int[]){5},(int[]){5},(int[]){5},(int[]){5},(int[]){6},(int[]){6},(int[]){6},(int[]){6},(int[]){7},(int[]){7},(int[]){8},(int[]){8}};
int transitionGuardsSizes[GROUPAMOUNT] = {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,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