Commit a1f1099c authored by point's avatar point
Browse files

New feature:

. add 'attribute id' formula in Acheck specifications that is the set of  transitions whose event contains a component with the attribute 'id'.
parent 0cd6b003
......@@ -353,6 +353,7 @@ s_interp_sgs_formula (altarica_tree *t, ar_sgs *sgs, int *is_state)
break;
case AR_TREE_LABEL :
case AR_TREE_EVENT_ATTRIBUTE :
{
ar_ca *ca = ar_sgs_get_constraint_automaton (sgs);
ar_node *node = ar_ca_get_node (ca);
......@@ -361,18 +362,27 @@ s_interp_sgs_formula (altarica_tree *t, ar_sgs *sgs, int *is_state)
ar_context_del_reference (ctx);
ar_node_del_reference (node);
if (ar_ca_has_subevent(ca, tmp))
if (IS_LABELLED_WITH (t, LABEL))
{
*is_state = 0;
sets[0] = ar_sgs_compute_label (sgs, tmp);
result = ar_sgs_formula_crt_cst (sets[0], *is_state);
if (ar_ca_has_subevent(ca, tmp))
{
*is_state = 0;
sets[0] = ar_sgs_compute_label (sgs, tmp);
result = ar_sgs_formula_crt_cst (sets[0], *is_state);
}
else
{
ccl_error("%s:%d: error: undefined event '", t->filename,
t->line);
ar_identifier_log (CCL_LOG_ERROR, tmp);
ccl_error ("'.\n");
}
}
else
{
ccl_error("%s:%d: error: undefined event '", t->filename,
t->line);
ar_identifier_log (CCL_LOG_ERROR, tmp);
ccl_error ("'.\n");
*is_state = 0;
sets[0] = ar_sgs_compute_attribute (sgs, tmp);
result = ar_sgs_formula_crt_cst (sets[0], *is_state);
}
ar_ca_del_reference (ca);
ar_identifier_del_reference (tmp);
......@@ -606,6 +616,7 @@ s_interp_state_or_transition_formula (altarica_tree *t, ar_sgs *sgs,
}
case AR_TREE_LABEL :
case AR_TREE_EVENT_ATTRIBUTE :
{
ar_ca *ca = ar_sgs_get_constraint_automaton (sgs);
ar_node *node = ar_ca_get_node (ca);
......@@ -614,17 +625,25 @@ s_interp_state_or_transition_formula (altarica_tree *t, ar_sgs *sgs,
ar_context_del_reference (ctx);
ar_node_del_reference (node);
if (ar_ca_has_subevent (ca, tmp))
if (IS_LABELLED_WITH (t, LABEL))
{
*is_state = 0;
result = ar_sgs_compute_label (sgs, tmp);
if (ar_ca_has_subevent (ca, tmp))
{
*is_state = 0;
result = ar_sgs_compute_label (sgs, tmp);
}
else
{
ccl_error("%s:%d: error: undefined event '", t->filename,
t->line);
ar_identifier_log (CCL_LOG_ERROR, tmp);
ccl_error ("'.\n");
}
}
else
{
ccl_error("%s:%d: error: undefined event '", t->filename,
t->line);
ar_identifier_log (CCL_LOG_ERROR, tmp);
ccl_error ("'.\n");
*is_state = 0;
result = ar_sgs_compute_attribute (sgs, tmp);
}
ar_ca_del_reference (ca);
ar_identifier_del_reference (tmp);
......
/*
* ar-mec5-relation.c -- add a comment about this file
* Copyright (C) 2008 A. Griffault, G. Point, A. Vincent, LaBRI, CNRS UMR 5800,
* Universite Bordeaux I
*
* This file is a part of the AltaRica Checker (ARC) project.
*
* Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the AltaRica Public License that comes with this
......
......@@ -205,6 +205,8 @@ static ar_sgs_set *
s_rs_state_set (ar_sgs *sgs, ar_ca_expr *cond);
static ar_sgs_set *
s_rs_label (ar_sgs *sgs, ar_identifier *label);
static ar_sgs_set *
s_rs_event_attribute (ar_sgs *sgs, ar_identifier *attribute);
static ccl_list *
s_rs_classes (ar_sgs *sgs);
static ar_sgs_set *
......@@ -305,6 +307,7 @@ static const struct ar_state_graph_semantics_methods_st RS_METHODS =
s_rs_coreach,
s_rs_state_set,
s_rs_label,
s_rs_event_attribute,
s_rs_classes,
s_rs_lfp,
s_rs_gfp,
......@@ -3477,6 +3480,32 @@ s_rs_label (ar_sgs *sgs, ar_identifier *label)
/* --------------- */
static ar_sgs_set *
s_rs_event_attribute (ar_sgs *sgs, ar_identifier *attribute)
{
int i;
ar_relsem *rs = RS (sgs);
ar_ca_event **events = ar_ca_get_events (rs->super.ca);
ar_sgs_set *R =
s_relsem_set_create (AR_SGS_SET_IS_TRANS, RS (sgs)->nb_events);
ar_dd zero = ar_dd_zero (rs->ddm);
for (i = 0; i < rs->nb_events; i++)
{
ar_dd set;
if (ar_ca_event_has_attribute (events[i], attribute))
set = rs->event_relations[i];
else
set = zero;
DD (R)[i] = AR_DD_DUP (set);
}
return R;
}
/* --------------- */
static ar_dd
s_dd_for_number (ar_relsem *rs, int value, int bit_index, int start_index)
{
......
......@@ -79,6 +79,7 @@ struct ar_state_graph_semantics_methods_st
ar_sgs_set * (*coreach) (ar_sgs *sgs, ar_sgs_set *S, ar_sgs_set *T);
ar_sgs_set * (*state_set) (ar_sgs *sgs, ar_ca_expr *cond);
ar_sgs_set * (*label) (ar_sgs *sgs, ar_identifier *label);
ar_sgs_set * (*event_attribute) (ar_sgs *sgs, ar_identifier *label);
ccl_list * (*classes) (ar_sgs *sgs);
ar_sgs_set * (*lfp) (ar_sgs *sgs, ar_identifier *var, ar_sgs_formula *F);
ar_sgs_set * (*gfp) (ar_sgs *sgs, ar_identifier *var, ar_sgs_formula *F);
......
......@@ -13,9 +13,9 @@
*/
/*
* $Author: point $
* $Revision: 1.8 $
* $Date: 2010/01/13 11:52:16 $
* $Id: ar-state-graph-semantics.c,v 1.8 2010/01/13 11:52:16 point Exp $
* $Revision: 1.9 $
* $Date: 2010/02/16 13:02:22 $
* $Id: ar-state-graph-semantics.c,v 1.9 2010/02/16 13:02:22 point Exp $
*/
#include <ccl/ccl-assert.h>
#include <ccl/ccl-memory.h>
......@@ -507,6 +507,17 @@ ar_sgs_compute_label (ar_sgs *sgs, ar_identifier *label)
/* --------------- */
ar_sgs_set *
ar_sgs_compute_attribute (ar_sgs *sgs, ar_identifier *attr)
{
ccl_pre (sgs != NULL);
ccl_pre (attr != NULL);
return sgs->methods->event_attribute (sgs, attr);
}
/* --------------- */
ccl_list *
ar_sgs_compute_classes (ar_sgs *sgs)
{
......
......@@ -13,9 +13,9 @@
*/
/*
* $Author: point $
* $Revision: 1.6 $
* $Date: 2010/01/13 11:52:16 $
* $Id: ar-state-graph-semantics.h,v 1.6 2010/01/13 11:52:16 point Exp $
* $Revision: 1.7 $
* $Date: 2010/02/16 13:02:22 $
* $Id: ar-state-graph-semantics.h,v 1.7 2010/02/16 13:02:22 point Exp $
*/
/*!
......@@ -147,6 +147,9 @@ ar_sgs_compute_state_set (ar_sgs *sgs, ar_ca_expr *cond);
extern ar_sgs_set *
ar_sgs_compute_label (ar_sgs *sgs, ar_identifier *label);
extern ar_sgs_set *
ar_sgs_compute_attribute (ar_sgs *sgs, ar_identifier *attr);
extern ccl_list *
ar_sgs_compute_classes (ar_sgs *sgs);
......
......@@ -26,25 +26,6 @@
* \brief
*
*/
/*
* ar-transition-system.c -- add a comment about this file
* Copyright (C) 2008 A. Griffault, G. Point, A. Vincent, LaBRI, CNRS UMR 5800,
* Universite Bordeaux I
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the AltaRica Public License that comes with this
* package.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*/
/*
* $Author: point $
* $Revision: 1.11 $
* $Date: 2010/01/13 11:52:16 $
* $Id: ar-transition-system.c,v 1.11 2010/01/13 11:52:16 point Exp $
*/
#include <ccl/ccl-assert.h>
#include "ar-transition-system-p.h"
#include "ar-ts-algorithms.h"
......@@ -113,6 +94,8 @@ static ar_sgs_set *
s_ts_state_set (ar_sgs *sgs, ar_ca_expr *cond);
static ar_sgs_set *
s_ts_label (ar_sgs *sgs, ar_identifier *label);
static ar_sgs_set *
s_ts_event_attribute (ar_sgs *sgs, ar_identifier *attribute);
static ccl_list *
s_ts_classes (ar_sgs *sgs);
static ar_sgs_set *
......@@ -161,6 +144,7 @@ static const struct ar_state_graph_semantics_methods_st TS_METHODS =
s_ts_coreach,
s_ts_state_set,
s_ts_label,
s_ts_event_attribute,
s_ts_classes,
s_ts_lfp,
s_ts_gfp,
......@@ -803,6 +787,14 @@ s_ts_label (ar_sgs *sgs, ar_identifier *label)
/* --------------- */
static ar_sgs_set *
s_ts_event_attribute (ar_sgs *sgs, ar_identifier *attribute)
{
return SGS_SET (ar_ts_compute_event_attribute (TS (sgs), attribute));
}
/* --------------- */
static ccl_list *
s_ts_classes (ar_sgs *sgs)
{
......
/* $Id: ar-ts-algorithms.h,v 1.6 2010/01/13 11:52:16 point Exp $ */
/*
* ar-ts-algorithms.h -- add a comment about this file
*
* This file is a part of the AltaRica Checker (ARC) project.
*
* Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the AltaRica Public License that comes with this
* package.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*/
/*!
* \file
* \brief
*
*/
#ifndef __AR_TS_ALGORITHMS_H__
# define __AR_TS_ALGORITHMS_H__
......@@ -44,6 +64,9 @@ ar_ts_compute_state_set(ar_ts *ts, ar_ca_expr *cond);
extern ar_ts_mark *
ar_ts_compute_label(ar_ts *ts, ar_identifier *label);
extern ar_ts_mark *
ar_ts_compute_event_attribute (ar_ts *ts, ar_identifier *attribute);
extern ccl_list *
ar_ts_compute_classes(ar_ts *ts);
......
/* $Id: ar-ts-atoms.c,v 1.3 2008/06/20 15:36:07 point Exp $ */
/*
* ar-ts-atoms.c -- add a comment about this file
*
* This file is a part of the AltaRica Checker (ARC) project.
*
* Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the AltaRica Public License that comes with this
* package.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*/
/*!
* \file
* \brief
*
*/
#include <ccl/ccl-assert.h>
#include "ar-transition-system-p.h"
#include "ar-ts-algorithms.h"
......@@ -152,6 +172,27 @@ ar_ts_compute_label(ar_ts *ts, ar_identifier *label)
ar_ts_mark_add(result,i);
}
return result;
}
/* --------------- */
ar_ts_mark *
ar_ts_compute_event_attribute (ar_ts *ts, ar_identifier *label)
{
int i;
ar_ts_mark *result;
ccl_pre (ts != NULL);
ccl_pre (label != NULL);
result = ar_ts_empty_trans_mark (ts);
for (i = 0; i < ts->nb_trans; i++)
{
if (ar_ca_event_has_attribute (ts->trans_table.data[i].label, label))
ar_ts_mark_add (result, i);
}
return result;
}
......@@ -32,7 +32,7 @@ void
ar_sequences_generator_with_dd (ar_node *flat, ar_ca *observer,
ar_ca_expr *acceptance)
{
ccl_list *counters = ccl_list_create ();
/* ccl_list *counters = ccl_list_create (); */
ar_relsem *rs;
ar_decorate_observer (flat, observer, NULL);
rs = ar_compute_relational_semantics(observer);
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment