Echtzeitsysteme/tchecker
1
0
Fork 0
mirror of https://github.com/Echtzeitsysteme/tchecker.git synced 2024-05-20 20:00:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

added first version of vcg

Browse source
This commit is contained in:
alzeha 2024-01-17 13:45:45 +01:00
parent dba572276d
commit 921ecab880
92 changed files with 5164 additions and 1635 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/build-and-test.yml vendored
View file

@ -2,7 +2,7 @@ name: Build and test TChecker
on:
push:
branches:
- '*'
- '**'
jobs:
build-and-test-linux:

25
CMakeLists.txt
View file

@ -5,6 +5,7 @@
cmake_minimum_required(VERSION 3.13)
set(LOCAL_CONFIG "${CMAKE_SOURCE_DIR}/localconfig-${CMAKE_BUILD_TYPE}.cmake")
if(EXISTS ${LOCAL_CONFIG})
cmake_policy(SET CMP0077 NEW)
message(STATUS "Loading ${LOCAL_CONFIG} file.")
@ -15,6 +16,30 @@ endif()
project(tchecker LANGUAGES CXX)
if (USE_CPPCHECK)
find_program(CMAKE_CXX_CPPCHECK NAMES cppcheck)
if(NOT ${CMAKE_CXX_CPPCHECK} STREQUAL "NOTFOUND")
message(STATUS "found CPPCHECK: ${CMAKE_CXX_CPPCHECK}")
message(STATUS "using CPPCHECK")
set(CPPCHECK_BUILD_DIR "${CMAKE_CURRENT_BINARY_DIR}/cppcheck-build-dir")
file(MAKE_DIRECTORY ${CPPCHECK_BUILD_DIR})
list(
APPEND CMAKE_CXX_CPPCHECK
"--enable=warning"
"--inconclusive"
"--force"
"--inline-suppr"
"--cppcheck-build-dir=${CPPCHECK_BUILD_DIR}"
"--error-exitcode=1"
"--suppressions-list=${CMAKE_SOURCE_DIR}/CppCheckSuppressions.txt"
)
else()
message(FATAL_ERROR "wanted to use CPPCHECK, but not installed")
endif()
else()
message(STATUS "CPP_CHECK is not actived. If you want to activate it, use -DUSE_CPPCHECK=1")
endif()
set(TCK_CMAKE_SCRIPT_DIR "${CMAKE_SOURCE_DIR}/cmake")
list(APPEND CMAKE_MODULE_PATH "${TCK_CMAKE_SCRIPT_DIR}")

19
CppCheckSuppressions.txt Normal file
View file

@ -0,0 +1,19 @@
// Won't fix
*:*/src/parsing/*
nullPointer:*/tchecker/src/refzg/refzg.cc:[181, 176, 189, 190, 197, 203, 208]
uninitdata:*/include/tchecker/utils/shared_objects.hh
nullPointer:*/src/refzg/refzg.cc
// TODO: fix the following
rethrowNoCurrentException:*/include/tchecker/variables/variables.hh
assertWithSideEffect:*/include/tchecker/variables/variables.hh
funcArgOrderDifferent:*/src/clockbounds/solver.cc
assertWithSideEffect:*/include/tchecker/waiting/waiting.hh
uninitMemberVar:*/src/algorithms/covreach/stats.cc
// TODO: decide whether to fix the following
operatorEqVarError:*/include/tchecker/utils/shared_objects.hh
missingMemberCopy:*/include/tchecker/utils/shared_objects.hh
// the following is a known cppcheck bug
internalAstError:*/include/tchecker/graph/directed_graph.hh

3
README.md
View file

@ -1,6 +1,5 @@
# TChecker
[![Build and test TChecker](https://github.com/ticktac-project/tchecker/actions/workflows/build-and-test.yml/badge.svg)](https://github.com/ticktac-project/tchecker/actions/workflows/build-and-test.yml)
[![License](https://img.shields.io/badge/license-MIT-informational.svg)](https://github.com/ticktac-project/tchecker/blob/master/LICENSE)
@ -24,6 +23,8 @@ community.
## Installation
Please note that this fork is only tested for Ubuntu.
Please, refer to [Installation of TChecker](https://github.com/ticktac-project/tchecker/wiki/Installation-of-TChecker) or to file INSTALL.md in the repository.
## Usage

23
ci-scripts/build-in-docker.sh
View file

@ -1,23 +0,0 @@
#!/bin/bash -x
SCRIPTDIR=$(cd $(dirname $0); pwd)
BUILDDIR=build/docker-${TCHECKER_DOCKER_IMAGE}
PROJECTROOT=$(cd ${SCRIPTDIR}/..; pwd)
error() {
echo "$0: error: $1." 1>&2
exit 1
}
${TCHECKER_DOCKER:-false} || error "not in a tcheker container"
cd ${PROJECTROOT}
export INSTALL_DIR=${BUILDDIR}/_inst
export TCHECKER_BUILD_TYPE=Debug
export CXX=g++
export CC=gcc
export CONFNAME=all:int64:memcheck
export VERBOSE=1
./ci-scripts/build.sh ${BUILDDIR}

1
ci-scripts/build.sh
View file

@ -63,6 +63,7 @@ cd ${BUILDDIR}
cmake -DCMAKE_INSTALL_PREFIX=${INSTALL_DIR} \
-DCMAKE_CXX_COMPILER=${CXX} \
-DCMAKE_BUILD_TYPE=${TCHECKER_BUILD_TYPE} \
-DUSE_CPPCHECK=1 \
${TEST_CONF} \
${SOURCEDIR}

20
ci-scripts/github-ubuntu-build-and-test-clang.sh
View file

@ -6,7 +6,21 @@ apt upgrade -y
export CC="clang"
export CXX="clang++"
./ci-scripts/build.sh
./ci-scripts/test.sh
chmod a+x ./ci-scripts/build.sh
chmod a+x ./ci-scripts/test.sh
chmod a+x ./ci-scripts/show-config.sh
./ci-scripts/show-config.sh
ci-scripts/build.sh
retn_code=$?
if [ $retn_code -ne 0 ]; then
exit $retn_code
fi
ci-scripts/test.sh
retn_code=$?
if [ $retn_code -ne 0 ]; then
exit $retn_code
fi
ci-scripts/show-config.sh

20
ci-scripts/github-ubuntu-build-and-test-gcc.sh
View file

@ -6,7 +6,21 @@ apt upgrade -y
export CC="gcc"
export CXX="g++"
./ci-scripts/build.sh
./ci-scripts/test.sh
chmod a+x ./ci-scripts/build.sh
chmod a+x ./ci-scripts/test.sh
chmod a+x ./ci-scripts/show-config.sh
./ci-scripts/show-config.sh
ci-scripts/build.sh
retn_code=$?
if [ $retn_code -ne 0 ]; then
exit $retn_code
fi
ci-scripts/test.sh
retn_code=$?
if [ $retn_code -ne 0 ]; then
exit $retn_code
fi
ci-scripts/show-config.sh

12
examples/missing_initial.sh Executable file
View file

@ -0,0 +1,12 @@
#!/bin/bash
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
echo "# labels=green"
echo "# Watch Out! This is an example on how NOT to create a model. The initial location is missing"
cat "$(dirname $0)/missing_initial.txt"

25
examples/missing_initial.txt Normal file
View file

@ -0,0 +1,25 @@
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
system:missing_initial
clock:1:x
clock:1:y
event:a
event:b
event:c
event:d
process:P
location:P:l0{}
location:P:l1{}
location:P:l2{}
location:P:l3{labels: green}
edge:P:l0:l1:a{do:y=0}
edge:P:l1:l2:b{provided: y==1}
edge:P:l1:l3:c{provided: x<1}
edge:P:l2:l3:c{provided: x<1}
edge:P:l3:l1:a{provided: y<1 : do:y=0}
edge:P:l3:l3:d{provided: x>1}

2
include/tchecker/basictypes.hh
View file

@ -15,6 +15,8 @@
#include <boost/rational.hpp>
#define VIRTUAL_CLOCK_PREFIX "chi"
/*!
\file basictypes.hh
\brief Definition of basic types for models

27
include/tchecker/dbm/dbm.hh
View file

@ -47,6 +47,19 @@ enum status_t {
MAY_BE_EMPTY,
};
/*!
\brief get dbm[i, j]
\return a pointer to dbm[i, j]
*/
const tchecker::dbm::db_t * access(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t i, tchecker::clock_id_t j);
/*!
\brief non const version of access
\return a pointer to dbm[i, j]
\note Watch Out what you are doing! There is no guarantee on anything!
*/
tchecker::dbm::db_t * access(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t i, tchecker::clock_id_t j);
/*!
\brief Copy a DBM into another DBM
\param dbm1 : target dbm
@ -571,6 +584,18 @@ void open_down(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim);
enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::dbm::db_t const * dbm1,
tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim);
/*!
\brief revert-multiple-reset function (see the TR of Lieb et al.)
\param orig_zone the previous zone
\param zone_split : the split of reset(orig_zone)
\param reset : the used reset set
\return the dbm with reverted resets (same dim as orig_zone)
\note the returned dbm is allocated on the heap. You have to free it!
*/
tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone,
tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split,
tchecker::clock_reset_container_t reset);
/*!
\brief ExtraM extrapolation
\param dbm : a dbm
@ -745,7 +770,7 @@ std::ostream & output(std::ostream & os, tchecker::dbm::db_t const * dbm, tcheck
\param dim1 : dimension of dbm1
\param dbm2 : second dbm
\param dim2 : dimension of dbm2
\pre dbm1 and dbm2 are ot nullptr (checked by assertion)
\pre dbm1 and dbm2 are not nullptr (checked by assertion)
dbm1 is a dim1*dim1 array of difference bounds
dbm2 is a dim2*dim2 array of difference bounds
dim1 >= 1 and dim2 >= 1 (checked by assertion)

69
include/tchecker/extrapolation/extrapolation.hh Normal file
View file

@ -0,0 +1,69 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_HH
#define TCHECKER_ZG_EXTRAPOLATION_HH
#include "tchecker/clockbounds/clockbounds.hh"
#include "tchecker/dbm/db.hh"
#include "tchecker/dbm/dbm.hh"
/*!
\file extrapolation.hh
\brief Zone extrapolations to ensure finiteness of zone graphs
*/
namespace tchecker {
namespace zg {
/*!
\class extrapolation_t
\brief Zone extrapolation
*/
class extrapolation_t {
public:
/*!
\brief Destructor
*/
virtual ~extrapolation_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\post dbm has been extrapolated using clocks bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) = 0;
};
/*!
\class no_extrapolation_t
\brief No zone extrapolation
*/
class no_extrapolation_t final : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Destructor
*/
virtual ~no_extrapolation_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\post dbm has not been modified
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
} // end of namespace zg
} // end of namespace tchecker
#endif // TCHECKER_ZG_EXTRAPOLATION_HH

91
include/tchecker/extrapolation/extrapolation_factory.hh Normal file
View file

@ -0,0 +1,91 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_FACTORY_HH
#define TCHECKER_ZG_EXTRAPOLATION_FACTORY_HH
#include "tchecker/clockbounds/clockbounds.hh"
#include "tchecker/ta/system.hh"
#include "tchecker/extrapolation/extrapolation.hh"
/*!
\file extrapolation.hh
\brief Zone extrapolations to ensure finiteness of zone graphs
*/
namespace tchecker {
namespace zg {
/*!
\brief Type of extrapolation
*/
enum extrapolation_type_t {
NO_EXTRAPOLATION, /*!< see tchecker::zg::no_extrapolation_t */
EXTRA_LU_GLOBAL, /*!< see tchecker::zg::global_extra_lu_t */
EXTRA_LU_LOCAL, /*!< see tchecker::zg::local_extra_lu_t */
EXTRA_LU_PLUS_GLOBAL, /*!< see tchecker::zg::global_extra_lu_plus_t */
EXTRA_LU_PLUS_LOCAL, /*!< see tchecker::zg::local_extra_lu_plus_t */
EXTRA_M_GLOBAL, /*!< see tchecker::zg::global_extra_m_t */
EXTRA_M_LOCAL, /*!< see tchecker::zg::local_extra_m_t */
EXTRA_M_PLUS_GLOBAL, /*!< see tchecker::zg::global_extra_m_plus_t */
EXTRA_M_PLUS_LOCAL, /*!< see tchecker::zg::local_extra_m_plus_t */
EXTRA_K_NORM /* see tchecker::zg::k_norm */
};
/*!
\brief Zone extrapolation factory
\param extrapolation_type : type of extrapolation
\param system : system of timed processes
\return a zone extrapolation of type extrapolation_type using clock bounds
inferred from system, nullptr if clock bounds cannot be inferred from system (see
tchecker::clockbounds::compute_clockbounds)
\note the returned extrapolation must be deallocated by the caller
\throw std::invalid_argument : if extrapolation_type is unknown
*/
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::ta::system_t const & system);
/*!
\brief Zone extrapolation factory
\param extrapolation_type : type of extrapolation
\param clock_bounds : clock bounds
\return a zone extrapolation of type extrapolation_type using clock bounds from
clock_bounds
\note the returned extrapolation must be deallocated by the caller
\throw std::invalid_argument : if extrapolation_type is unknown
*/
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::clockbounds::clockbounds_t const & clock_bounds);
} // end of namespace zg
namespace vcg {
/*!
\brief Zone extrapolation factory
\param extrapolation_type : type of extrapolation
\param orig_system_first : first system of timed processes
\param orig_system_secpmd : second system of timed processes
\param first_not_second : true iff this vcg is the left hand side of the comparison
\return a zone extrapolation of type extrapolation_type using clock bounds
inferred from the systems, nullptr if clock bounds cannot be inferred from system (see
tchecker::clockbounds::compute_clockbounds)
\note the returned extrapolation must be deallocated by the caller
\throw std::invalid_argument : if extrapolation_type is unknown
*/
tchecker::zg::extrapolation_t * extrapolation_factory(
enum tchecker::zg::extrapolation_type_t type,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_first,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_second,
bool first_not_second);
} // end of namespace vcg
} // end of namespace tchecker
#endif // TCHECKER_ZG_EXTRAPOLATION_HH

115
include/tchecker/extrapolation/global_lu_extrapolation.hh Normal file
View file

@ -0,0 +1,115 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_GLOBAL_LU_EXTRAPOLATION_HH
#define TCHECKER_ZG_EXTRAPOLATION_GLOBAL_LU_EXTRAPOLATION_HH
#include "tchecker/extrapolation/extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
/*!
\class global_lu_extrapolation_t
\brief Zone extrapolation with global LU clock bounds (abstract class)
*/
class global_lu_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : global LU clock bounds map
*/
global_lu_extrapolation_t(std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
global_lu_extrapolation_t(tchecker::zg::details::global_lu_extrapolation_t const & e) = default;
/*!
\brief Move constructor
*/
global_lu_extrapolation_t(tchecker::zg::details::global_lu_extrapolation_t && e) = default;
/*!
\brief Destructor
*/
virtual ~global_lu_extrapolation_t() = default;
/*!
\brief Assignment operator
*/
tchecker::zg::details::global_lu_extrapolation_t &
operator=(tchecker::zg::details::global_lu_extrapolation_t const & e) = default;
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::global_lu_extrapolation_t & operator=(tchecker::zg::details::global_lu_extrapolation_t && e) = default;
protected:
std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> _clock_bounds; /*!< global LU clock bounds map */
};
} // end of namespace details
/*!
\class global_extra_lu_t
\brief ExtraLU zone extrapolation with global LU clock bounds
*/
class global_extra_lu_t : public tchecker::zg::details::global_lu_extrapolation_t {
public:
using tchecker::zg::details::global_lu_extrapolation_t::global_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_lu_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU has been applied to dbm with global LU clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) final;
};
/*!
\class global_extra_lu_plus_t
\brief ExtraLU+ zone extrapolation with global LU clock bounds
*/
class global_extra_lu_plus_t final : public tchecker::zg::details::global_lu_extrapolation_t {
public:
using tchecker::zg::details::global_lu_extrapolation_t::global_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_lu_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU+ has been applied to dbm with global LU clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
} // enf of namespace zg
} // end of namespace tchecker
#endif

117
include/tchecker/extrapolation/global_m_extrapolation.hh Normal file
View file

@ -0,0 +1,117 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_GLOBAL_M_EXTRAPOLATION_HH
#define TCHECKER_ZG_EXTRAPOLATION_GLOBAL_M_EXTRAPOLATION_HH
#include "tchecker/extrapolation/extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
/*!
\class global_m_extrapolation_t
\brief Zone extrapolation with global M clock bounds (abstract class)
*/
class global_m_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : global M clock bounds map
*/
global_m_extrapolation_t(std::shared_ptr<tchecker::clockbounds::global_m_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
global_m_extrapolation_t(tchecker::zg::details::global_m_extrapolation_t const & e) = default;
/*!
\brief Move constructor
*/
global_m_extrapolation_t(tchecker::zg::details::global_m_extrapolation_t && e) = default;
/*!
\brief Destructor
*/
virtual ~global_m_extrapolation_t() = default;
/*!
\brief Assignment operator
*/
tchecker::zg::details::global_m_extrapolation_t &
operator=(tchecker::zg::details::global_m_extrapolation_t const & e) = default;
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::global_m_extrapolation_t & operator=(tchecker::zg::details::global_m_extrapolation_t && e) = default;
protected:
std::shared_ptr<tchecker::clockbounds::global_m_map_t const> _clock_bounds; /*!< global LU clock bounds map */
};
} // end of namespace details
/*!
\class global_extra_m_t
\brief ExtraM zone extrapolation with global M clock bounds
*/
class global_extra_m_t final : public tchecker::zg::details::global_m_extrapolation_t {
public:
using tchecker::zg::details::global_m_extrapolation_t::global_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_m_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM has been applied to dbm with global M clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class global_extra_m_plus_t
\brief ExtraM+ zone extrapolation with global M clock bounds
*/
class global_extra_m_plus_t final : public tchecker::zg::details::global_m_extrapolation_t {
public:
using tchecker::zg::details::global_m_extrapolation_t::global_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_m_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM+ has been applied to dbm with global M clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
} // end of namespace zg
} // end of namespace tchecker
#endif

67
include/tchecker/extrapolation/k_norm.hh Normal file
View file

@ -0,0 +1,67 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_K_NORM_HH
#define TCHECKER_ZG_EXTRAPOLATION_K_NORM_HH
#include "tchecker/extrapolation/extrapolation.hh"
#include "tchecker/extrapolation/global_lu_extrapolation.hh"
namespace tchecker {
namespace zg {
/*!
\class k_norm
\brief K-Normalization for zone extrapolation
*/
class k_norm final : public tchecker::zg::global_extra_lu_t {
public:
/*!
\brief Constructor
\param clock_bounds : global LU clock bounds map
\note WARNING: we change the clock bounds, ignoring the const statement
*/
k_norm(std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds);
/*!
\brief Destructor
*/
virtual ~k_norm() = default;
using tchecker::zg::global_extra_lu_t::extrapolate;
};
} // end of namespace zg
namespace vcg {
class k_norm_virtual final : public tchecker::zg::global_extra_lu_t {
public:
/*!
\brief Constructor
\param clock_bounds : global LU clock bounds map
\note WARNING: we change the clock bounds, ignoring the const statement
*/
k_norm_virtual(std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds);
/*!
\brief Destructor
*/
virtual ~k_norm_virtual() = default;
using tchecker::zg::global_extra_lu_t::extrapolate;
};
} // end of namespace vcg
} // end of namespace tchecker
#endif

116
include/tchecker/extrapolation/local_lu_extrapolation.hh Normal file
View file

@ -0,0 +1,116 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_LOCAL_LU_EXTRAPOLATION_HH
#define TCHECKER_ZG_EXTRAPOLATION_LOCAL_LU_EXTRAPOLATION_HH
#include "tchecker/extrapolation/extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
/*!
\class local_lu_extrapolation_t
\brief Zone extrapolation with local LU clock bounds (abstract class)
*/
class local_lu_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : local LU clock bounds map
*/
local_lu_extrapolation_t(std::shared_ptr<tchecker::clockbounds::local_lu_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t const & e);
/*!
\brief Move constructor
*/
local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t && e);
/*!
\brief Destructor
*/
virtual ~local_lu_extrapolation_t();
/*!
\brief Assignment operator
*/
tchecker::zg::details::local_lu_extrapolation_t & operator=(tchecker::zg::details::local_lu_extrapolation_t const & e);
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::local_lu_extrapolation_t & operator=(tchecker::zg::details::local_lu_extrapolation_t && e);
protected:
tchecker::clockbounds::map_t * _l; /*!< clock bounds L map */
tchecker::clockbounds::map_t * _u; /*!< clock bounds U map */
std::shared_ptr<tchecker::clockbounds::local_lu_map_t const> _clock_bounds; /*!< local LU clock bounds map */
};
} // end of namespace details
/*!
\class local_extra_lu_t
\brief ExtraLU zone extrapolation with local LU clock bounds
*/
class local_extra_lu_t final : public tchecker::zg::details::local_lu_extrapolation_t {
public:
using tchecker::zg::details::local_lu_extrapolation_t::local_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_lu_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU has been applied to dbm with local LU clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class local_extra_lu_plus_t
\brief ExtraLU+ zone extrapolation with local LU clock bounds
*/
class local_extra_lu_plus_t final : public tchecker::zg::details::local_lu_extrapolation_t {
public:
using tchecker::zg::details::local_lu_extrapolation_t::local_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_lu_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU+ has been applied to dbm with local LU clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
} // end of namespace zg
} // end of namespace tchecker
#endif

111
include/tchecker/extrapolation/local_m_extrapolation.hh Normal file
View file

@ -0,0 +1,111 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/extrapolation/extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
/*!
\class local_m_extrapolation_t
\brief Zone extrapolation with local M clock bounds (abstract class)
*/
class local_m_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : local M clock bounds map
*/
local_m_extrapolation_t(std::shared_ptr<tchecker::clockbounds::local_m_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t const & e);
/*!
\brief Move constructor
*/
local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t && e);
/*!
\brief Destructor
*/
virtual ~local_m_extrapolation_t();
/*!
\brief Assignment operator
*/
tchecker::zg::details::local_m_extrapolation_t & operator=(tchecker::zg::details::local_m_extrapolation_t const & e);
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::local_m_extrapolation_t & operator=(tchecker::zg::details::local_m_extrapolation_t && e);
protected:
tchecker::clockbounds::map_t * _m; /*!< clock bounds M map */
std::shared_ptr<tchecker::clockbounds::local_m_map_t const> _clock_bounds; /*!< local M clock bounds map */
};
} // end of namespace details
/*!
\class local_extra_m_t
\brief ExtraM zone extrapolation with local M clock bounds
*/
class local_extra_m_t final : public tchecker::zg::details::local_m_extrapolation_t {
public:
using tchecker::zg::details::local_m_extrapolation_t::local_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_m_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM has been applied to dbm with local M clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class local_extra_m_plus_t
\brief ExtraM+ zone extrapolation with local M clock bounds
*/
class local_extra_m_plus_t final : public tchecker::zg::details::local_m_extrapolation_t {
public:
using tchecker::zg::details::local_m_extrapolation_t::local_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_m_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM+ has been applied to dbm with local M clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
} // end of namespace zg
} // end of namespace tchecker

2
include/tchecker/parsing/parsing.hh
View file

@ -84,7 +84,7 @@ public:
/*!
\brief Destructor
*/
~attributes_parser_t() = default;
virtual ~attributes_parser_t() = default;
/*!
\brief Assignment operator

77
include/tchecker/strong-timed-bisim/stats.hh Normal file
View file

@ -0,0 +1,77 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ALGORITHMS_COMPARE_STATS_HH
#define TCHECKER_ALGORITHMS_COMPARE_STATS_HH
#include "tchecker/algorithms/stats.hh"
/*!
\file stats.hh
\brief Statistics for comparison algorithm
*/
namespace tchecker {
namespace strong_timed_bisim {
/*!
\class stats_t
\brief Statistics for comparison algorithm
*/
class stats_t : public tchecker::algorithms::stats_t {
public:
/*!
\brief Constructor
*/
stats_t();
/*!
\brief Accessor
\return A reference to the number of visited pair of states
*/
unsigned long visited_pair_of_states() const;
/*!
\brief Accessor
\return Number of visited transitions
*/
unsigned long visited_transitions() const;
/*!
\brief Accessor
\return The deepest path checked
*/
unsigned long deepest_path() const;
/*!
\brief Accessor
\return Reference to the answer whether the relationship is fulfilled
*/
bool relationship_fulfilled() const;
/*!
\brief Extract statistics as attributes (key, value)
\param m : attributes map
\post every statistics has been added to m
*/
void attributes(std::map<std::string, std::string> & m) const;
private:
unsigned long _visited_pair_of_states; /*!< Number of visited pairs of states */
unsigned long _visited_transitions; /*!< Number of visited transitions */
unsigned long _deepest_path; /*!< Number of visited transitions */
bool _relationship_fulfilled; /*< Whether the relationship is fulfilled */
};
} // end of namespace strong_timed_bisim
} // end of namespace tchecker
#endif // TCHECKER_ALGORITHMS_COMPARE_STATS_HH

48
include/tchecker/strong-timed-bisim/system.hh Normal file
View file

@ -0,0 +1,48 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_STRONG_TIMED_BISIM_SYSTEM_HH
#define TCHECKER_STRONG_TIMED_BISIM_SYSTEM_HH
#include "tchecker/ta/system.hh"
namespace tchecker {
namespace strong_timed_bisim {
class system_virtual_clocks_t : public tchecker::ta::system_t {
public:
/*!
\brief Constructor
*/
system_virtual_clocks_t(tchecker::ta::system_t const & system, std::size_t no_of_virtual_clocks, bool first_not_second);
/*!
\brief Accessor
\return the number of virtual clocks
*/
tchecker::clock_id_t get_no_of_virtual_clocks() const;
private:
// we disallow the standard constructor
system_virtual_clocks_t();
bool _first_not_second;
tchecker::clock_id_t _no_of_virtual_clocks;
using tchecker::ta::system_t::add_clock;
};
} // end of namespace strong_timed_bisim
} // end of namespace tchecker
#endif

97
include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh Normal file
View file

@ -0,0 +1,97 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ALGORITHMS_REACH_ALGORITHM_HH
#define TCHECKER_ALGORITHMS_REACH_ALGORITHM_HH
#include "tchecker/strong-timed-bisim/stats.hh"
#include "tchecker/vcg/vcg.hh"
#include "tchecker/utils/zone_container.hh"
namespace tchecker {
namespace strong_timed_bisim {
/*
\ class Lieb_et_al
\brief Implements the on-the-fly algorithm to check strong timed bisimulation of Lieb et al.
*/
class Lieb_et_al {
public:
Lieb_et_al() = delete;
/*!
\brief Constructor
\param input_first : the vcg of the first TA
\param input_second : the vcg of the second TA
*/
Lieb_et_al(std::shared_ptr<tchecker::vcg::vcg_t> input_first, std::shared_ptr<tchecker::vcg::vcg_t> input_second);
/*!
\brief running the algorithm of Lieb et al. (TODO: add paper ref here)
\param input_first : the first vcg
\param input_second : the second vcg
*/
tchecker::strong_timed_bisim::stats_t run();
private:
/*!
\brief check-for-outgoing-transitions-impl function of Lieb et al.
\param symb_state_first : the symbolic state that belongs to the first vcg
\param vcg_first : the first vcg
\param symb_state_second : the symbolic state that belongs to the second vcg
\param vcg_second : the second vcg
\param func : a function that takes two symbolic states and returns a list of virtual constraint
\return a list of virtual constraints that cannot be simulated.
\note the result is allocated at the heap and must be freed.
*/
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t symb_state_first,
std::shared_ptr<tchecker::vcg::vcg_t> vcg_first,
tchecker::zg::const_state_sptr_t symb_state_second,
std::shared_ptr<tchecker::vcg::vcg_t> vcg_second,
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
(*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t));
/*
\brief calling check_for_outgoing_transitions with first = A
*/
inline std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
check_for_outgoing_transitions_of_A( tchecker::zg::const_state_sptr_t symb_state_A,
tchecker::zg::const_state_sptr_t symb_state_B,
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
(*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t))
{
return check_for_outgoing_transitions(symb_state_A, _A, symb_state_B, _B, func);
}
/*
\brief calling check_for_outgoing_transitions with first = B
*/
inline std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
check_for_outgoing_transitions_of_B( tchecker::zg::const_state_sptr_t symb_state_A,
tchecker::zg::const_state_sptr_t symb_state_B,
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
(*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t))
{
return check_for_outgoing_transitions(symb_state_B, _B, symb_state_A, _A, func);
}
const std::shared_ptr<tchecker::vcg::vcg_t> _A;
const std::shared_ptr<tchecker::vcg::vcg_t> _B;
};
} // end of namespace strong_timed_bisim
} // end of namespace tchecker
#endif

4
include/tchecker/syncprod/system.hh
View file

@ -32,7 +32,7 @@ namespace syncprod {
\class system_t
\brief System of processes
*/
class system_t : private tchecker::system::system_t, private tchecker::syncprod::labels_t {
class system_t : public tchecker::system::system_t, private tchecker::syncprod::labels_t {
/*!
\brief Type of collection of asynchronous edges
*/
@ -94,6 +94,7 @@ public:
using tchecker::system::system_t::clock_variables;
using tchecker::system::system_t::clocks_count;
using tchecker::system::system_t::is_clock;
using tchecker::system::system_t::add_clock;
// Edges
using tchecker::system::system_t::edge;
@ -233,7 +234,6 @@ public:
private:
// Hidden modifiers
using tchecker::syncprod::labels_t::add_label;
using tchecker::system::system_t::add_clock;
using tchecker::system::system_t::add_edge;
using tchecker::system::system_t::add_event;
using tchecker::system::system_t::add_intvar;

17
include/tchecker/syncprod/vedge.hh
View file

@ -162,7 +162,24 @@ public:
*/
const_array_iterator_t end_array() const;
/*!
\brief This function checks whether all events of this are also
contained by other and vice versa.
\param my_system : the system this belongs to
\param other : the other transition
\param other_system: the system other belongs to
*/
bool event_equal(tchecker::system::system_t const & my_system, const vedge_t & other, tchecker::system::system_t const & other_system) const
{ return this->contains_events(my_system, other, other_system) && other.contains_events(other_system, *this, my_system); }
protected:
/*!
\brief checks, whether this contains transitions with all events of other
\param other : the other transition
*/
bool contains_events(const tchecker::system::system_t & my_system, const vedge_t & other, const tchecker::system::system_t & other_system) const;
/*!
\brief Constructor
\param size : size of vector of edges

8
include/tchecker/system/clock.hh
View file

@ -49,7 +49,13 @@ public:
\return number of declared clock variables if kind = tchecker::VK_DECLARED,
number of flattened clock variables if kind = tchecker::VK_FLATTENED
*/
inline std::size_t clocks_count(enum tchecker::variable_kind_t kind) const { return _clock_variables.size(kind); }
inline tchecker::clock_id_t clocks_count(enum tchecker::variable_kind_t kind) const {
std::size_t tmp = _clock_variables.size(kind);
if( tmp > std::numeric_limits<tchecker::clock_id_t>::max() ) {
throw std::runtime_error("you are using more clocks than allowed");
}
return static_cast<tchecker::clock_id_t>( tmp );
}
/*!
\brief Accessor

3
include/tchecker/ta/system.hh
View file

@ -37,7 +37,7 @@ namespace ta {
\class system_t
\brief System of processes for timed automata
*/
class system_t : private tchecker::syncprod::system_t {
class system_t : public tchecker::syncprod::system_t {
public:
/*!
\brief Constructor
@ -103,6 +103,7 @@ public:
using tchecker::syncprod::system_t::clock_variables;
using tchecker::syncprod::system_t::clocks_count;
using tchecker::syncprod::system_t::is_clock;
using tchecker::system::system_t::add_clock;
// Edges
using tchecker::syncprod::system_t::asynchronous_incoming_edges;

201
include/tchecker/utils/zone_container.hh Normal file
View file

@ -0,0 +1,201 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_ZONE_CONTAINER_HH
#define TCHECKER_ZG_ZONE_CONTAINER_HH
#include <iterator>
#include "tchecker/zg/zone.hh"
#include "tchecker/vcg/virtual_constraint.hh"
namespace tchecker {
// forward declaration
namespace virtual_constraint {
class virtual_constraint_t;
}
/*
\brief a container for all subtypes of zone
*/
template <typename T>
class zone_container_t {
public:
/*!
\brief Constructor
\param dim : dimension
*/
zone_container_t(tchecker::clock_id_t dim) : _dim(dim){ }
/*!
\brief Copy Constructor
\param container : the container to copy
*/
zone_container_t(zone_container_t &t) : _dim(t.dim()), _storage(0)
{
for(auto iter = t.begin(); iter < t.end(); iter++) {
this->append_zone(*(*iter));
}
}
/*!
\brief Accessor
*/
tchecker::clock_id_t dim() {return this->_dim;}
/*!
\brief factory functions to be used by the append functions
\note need for specialisation here!
*/
std::shared_ptr<T> create_element();
std::shared_ptr<T> create_element(T const &zone);
/*!
\brief destructor of zone. Calling the destructor of tchecker::zg::zone_t
\note If T extends tchecker::zg::zone_t by a datastructure, there is a need for
specialisation here!
*/
void destruct_element(std::shared_ptr<T> zone)
{
tchecker::zg::zone_destruct_and_deallocate(&(*zone));
}
/*
\brief check for emptiness of the container
\return true if and only if the container is empty
*/
bool is_empty()
{
return 0 == _storage.size();
}
/*!
\brief adds an universal zone to the container
*/
void append_zone()
{
_storage.emplace_back(create_element());
}
/*!
\brief adds a copy of the zone to the container
*/
void append_zone(T const & zone)
{
_storage.emplace_back(create_element(zone));
}
/*!
\brief adds the pointer to the container
\pre *zone must be initialised
\post zone is part of the container
*/
void append_zone(std::shared_ptr<T> zone)
{
_storage.emplace_back(zone);
}
/*!
\brief removes the last zone and deletes the content
*/
void remove_back()
{
destruct_element(*(_storage.begin()));
_storage.erase(_storage.begin());
}
/*!
\brief gets the the last zone
\return the pointer to that zone
*/
std::shared_ptr<T> back()
{
return _storage.back();
}
/*!
\brief Accessor of the ith element
\param i : the index to access
\return a ptr to the ith element
*/
std::shared_ptr<T> operator[](typename std::vector<std::shared_ptr<T>>::size_type i)
{
return _storage[i];
}
/*!
\brief Accessor
\return the number of elements stored in this container
*/
typename std::vector<std::shared_ptr<T>>::size_type size()
{
return _storage.size();
}
/*!
\brief returns an iterator, starting the begining, iterating over ptrs of zone_t
*/
typename std::vector<std::shared_ptr<T>>::iterator begin()
{
return _storage.begin();
}
/*!
\brief returns an iterator, starting after the end, iterating over ptrs of zone_t
*/
typename std::vector<std::shared_ptr<T>>::iterator end()
{
return _storage.end();
}
/*!
\brief Destructor
*/
~zone_container_t()
{
for(auto iter = begin(); iter < end(); ++iter) {
destruct_element(*iter);
}
}
private:
const tchecker::clock_id_t _dim;
std::vector<std::shared_ptr<T>> _storage;
};
// specializations
template<>
std::shared_ptr<tchecker::zg::zone_t> zone_container_t<tchecker::zg::zone_t>::create_element();
template<>
std::shared_ptr<tchecker::zg::zone_t> zone_container_t<tchecker::zg::zone_t>::create_element(tchecker::zg::zone_t const & zone);
template<>
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>::create_element();
template<>
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>::create_element(tchecker::virtual_constraint::virtual_constraint_t const & zone);
/*!
\brief contained-in-all function (see the TR of Lieb et al.)
\param a vector of vector of zones
\return a vector of zones
*/
zone_container_t<tchecker::zg::zone_t> contained_in_all(std::vector<zone_container_t<tchecker::zg::zone_t>> & zones, tchecker::clock_id_t dim);
} // end of namespace tchecker
#endif

39
include/tchecker/vcg/revert_transitions.hh Normal file
View file

@ -0,0 +1,39 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_VCG_REVERT_TRANSITIONS_HH
#define TCHECKER_VCG_REVERT_TRANSITIONS_HH
#include "tchecker/vcg/virtual_constraint.hh"
#include "tchecker/zg/zone.hh"
/*!
\brief revert-action-trans function (see the TR of Lieb et al.)
\param zone : the original zone
\param guard : of the transition to revert
\param reset : the reset set of the transition to revert
\param tgt_invariant : the invariant of the target state of the transition to revert
\param phi_split : the sub vc of the target
\return a shared pointer to the resulting virtual constraint
*/
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
revert_action_trans(const tchecker::zg::zone_t & zone,
const tchecker::clock_constraint_container_t & guard,
const tchecker::clock_reset_container_t & reset,
const tchecker::clock_constraint_container_t & tgt_invariant,
const tchecker::virtual_constraint::virtual_constraint_t & phi_split);
/*!
\brief revert-epsilon-trans function (see the TR of Lieb et al.)
\param zone : the original zone
\param phi_split : the sub vc of the target
\return a shared pointer to the resulting virtual constraint
*/
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split);
#endif

66
include/tchecker/vcg/sync.hh Normal file
View file

@ -0,0 +1,66 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_VCG_SYNC_HH
#define TCHECKER_VCG_SYNC_HH
#include "virtual_constraint.hh"
namespace tchecker {
namespace vcg {
/*!
\brief sync function (see the TR of Lieb et al.)
\param dbm1 : a dbm
\param dbm2 : a dbm
\param dim : dimension of dbm1 and dbm2
\param lowest_virt_clk_id : the clk id of chi_0
\param no_of_orig_clocks_1 : the number of orig clocks in the first TA
\param orig_reset1 : the resets of the transition of the first TA
\param orig_reset2 : the resets of the transition of the second TA
\pre dbm1 and dbm2 are not nullptr (checked by assertion)
dbm, dbm1 and dbm2 are dim*dim arrays of difference bounds
dbm1 and dbm2 are consistent (checked by assertion)
dbm1 and dbm2 are tight (checked by assertion)
dim >= 1 (checked by assertion).
\post dbm1 and dbm2 are synced, consistent and tight
\note the change happens inplace
*/
void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim,
tchecker::clock_id_t lowest_virt_clk_id, tchecker::clock_id_t no_of_orig_clocks_1,
tchecker::clock_reset_container_t const & orig_reset1,
tchecker::clock_reset_container_t const & orig_reset2);
/*!
\brief revert-sync function (see the TR of Lieb et al.)
\param dbm1 : a dbm
\param dbm2 : a dbm
\param dim : dimension of dbm1 and dbm2
\param lowest_virt_clk_id : the clk id of chi_0
\param no_of_orig_clocks_1 : the number of orig clocks in the first TA
\pre dbm1 and dbm2 are not nullptr (checked by assertion)
dbm, dbm1 and dbm2 are dim*dim arrays of difference bounds
dbm1 and dbm2 are consistent (checked by assertion)
dbm1 and dbm2 are tight (checked by assertion)
dim >= 1 (checked by assertion).
\post dbm1 and dbm2 are synced, consistent and tight
\note the change happens inplace. this function works if and only if only
resets to zero are allowed!
*/
std::tuple<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>>
revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim,
const tchecker::virtual_constraint::virtual_constraint_t & phi_e, tchecker::clock_id_t lowest_virt_clk_id,
tchecker::clock_id_t no_of_orig_clocks_1);
} // end of namespace vcg
} // end of namespace tchecker
#endif

87
include/tchecker/vcg/vcg.hh Normal file
View file

@ -0,0 +1,87 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_VCG_HH
#define TCHECKER_VCG_HH
#include "tchecker/strong-timed-bisim/system.hh"
#include "tchecker/zg/zg.hh"
#include "tchecker/zg/zone.hh"
/*!
\file vcg.hh
\brief Virtual Clock Graphs
*/
namespace tchecker {
namespace vcg {
/*!
\class vcg_t
\brief Transition system of the virtual clock graph over system of timed processes with
state and transition allocation
\note all returned states and transitions are deallocated automatically. A vcg is a zg
* with some extensions.
*/
class vcg_t : public tchecker::zg::zg_t {
public:
/*!
\brief Constructor
\param system : a system of timed processes
\param sharing_type : type of state/transition sharing
\param semantics : a zone semantics
\param no_of_virtual_clocks : number of virtual clocks
\param extrapolation : a zone extrapolation
\param block_size : number of objects allocated in a block
\param table_size : size of hash tables
\note all states and transitions are pool allocated and deallocated automatically
*/
vcg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
std::shared_ptr<tchecker::zg::semantics_t> const & semantics, tchecker::clock_id_t no_of_virtual_clocks,
std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size);
/*!
\brief Accessor
\return the number of virtual clocks
*/
tchecker::clock_id_t get_no_of_virtual_clocks() const;
private:
tchecker::clock_id_t _no_of_virtual_clocks;
};
/*!
\brief Factory of vcg with clock bounds computed from system
\param extended_system : the system with virtual clocks
\param first_not_second : true iff the extended system corresponds to the left hand side of the comparison
\param orig_system_first : the left hand side of the comparison
\param orig_system_second : the right hand side of the comparison
\param sharing_type : type of sharing
\param semantics_type : type of zone semantics
\param extrapolation_type : type of zone extrapolation (currently, k_norm only!)
\param block_size : number of objects allocated in a block
\param table_size : size of hash tables
\return a vcg over system with zone semantics and zone extrapolation
defined from semantics_type and extrapolation_type, and allocation of
block_size objects at a time, nullptr if clock bounds cannot be inferred from
system
*/
tchecker::vcg::vcg_t * factory(std::shared_ptr<tchecker::strong_timed_bisim::system_virtual_clocks_t const> const & extended_system,
bool first_not_second,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_first,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_second,
enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size,
std::size_t table_size) ;
} // end of namespace vcg
} // end of namespace tchecker
#endif

118
include/tchecker/vcg/virtual_constraint.hh Normal file
View file

@ -0,0 +1,118 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_VCG_VIRTUAL_CONSTRAINT_HH
#define TCHECKER_VCG_VIRTUAL_CONSTRAINT_HH
#include "tchecker/zg/zone.hh"
#include "tchecker/dbm/dbm.hh"
#include "tchecker/utils/zone_container.hh"
/*
\file virtual_constraint.hh
\brief our model of a virtual constraint
*/
namespace tchecker {
// forward declaration
template <typename T>
class zone_container_t;
namespace virtual_constraint {
/*!
\class virtual_constraint_t
\brief Implementation of virtual constraints
\note We model the virtual constraint as zone
* using the virtual clocks, only. This is
* fine since a zone always corresponds to a
* clock constraint
*/
class virtual_constraint_t : public tchecker::zg::zone_t {
public:
/*!
\brief delete all constructors, instantiate this class using a factory function
*/
virtual_constraint_t() = delete;
/*!
\brief Destructor
*/
~virtual_constraint_t() = default;
/*!
\brief Accessor
\return no of virtual clocks
*/
const tchecker::clock_id_t get_no_of_virt_clocks() const;
/*!
\brief return the virtual constraint as list of clock constraints
\param sum_of_orig_clocks : the sum of the original clocks of both TA
*/
clock_constraint_container_t get_vc(tchecker::clock_id_t orig_clocks_offset) const;
/*!
\brief returns the negated version of this clock constraint
\return let result be the return value.
* forall u with u model this and for all vc in result u does not model vc
* forall u with u does not model this exists a vc in result such that u models vc
* (for u in ({\chi_0, ..., \chi_{|C_A| + | C_B| - 1}} \rightarrow T))
*/
tchecker::zone_container_t<virtual_constraint_t> * neg() const;
/*
\brief iterates through the container and logically ands each element with this
\param container : the container to and with
\return a copy of container with each element being logically anded with this.
*/
tchecker::zone_container_t<virtual_constraint_t> logic_and(tchecker::zone_container_t<virtual_constraint_t> *container);
};
// factories
std::shared_ptr<virtual_constraint_t> factory(tchecker::clock_id_t dim);
std::shared_ptr<virtual_constraint_t> factory(tchecker::virtual_constraint::virtual_constraint_t const & virtual_constraint);
/*!
\brief extract the virtual constraint from a zone
\param zone : the zone from which the virtual constraint should be extracted
\param virtual_clocks : the number of virtual clocks
\return the virtual constraint of zone
*/
std::shared_ptr<virtual_constraint_t> factory(std::shared_ptr<tchecker::zg::zone_t const> zone, tchecker::clock_id_t no_of_virtual_clocks);
/*!
\brief extract the virtual constraint from a dbm
\param dbm : the dbm from which the virtual constraint should be extracted
\param dim : dimension of the dbm
\param virtual_clocks : the number of virtual clocks
\return the virtual constraint of zone
*/
std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virtual_clocks);
// destruction
void destruct(virtual_constraint_t *to_destruct);
/*!
\brief combine operator (see the TR of Lieb et al.)
\param a vector of vector of virtual constraints
\return a vector of virtual constraints
*/
tchecker::zone_container_t<virtual_constraint_t> *combine(std::vector<tchecker::zone_container_t<virtual_constraint_t>> & lo_lo_vc, tchecker::clock_id_t dim);
} // end of namespace virtual_constraint
} // end of namespace tchecker
#endif

492
include/tchecker/zg/extrapolation.hh
View file

@ -1,492 +0,0 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_HH
#define TCHECKER_ZG_EXTRAPOLATION_HH
#include <memory>
#include "tchecker/basictypes.hh"
#include "tchecker/clockbounds/clockbounds.hh"
#include "tchecker/dbm/db.hh"
#include "tchecker/dbm/dbm.hh"
#include "tchecker/syncprod/vloc.hh"
#include "tchecker/ta/system.hh"
/*!
\file extrapolation.hh
\brief Zone extrapolations to ensure finiteness of zone graphs
*/
namespace tchecker {
namespace zg {
/*!
\class extrapolation_t
\brief Zone extrapolation
*/
class extrapolation_t {
public:
/*!
\brief Destructor
*/
virtual ~extrapolation_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\post dbm has been extrapolated using clocks bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) = 0;
};
/*!
\class no_extrapolation_t
\brief No zone extrapolation
*/
class no_extrapolation_t final : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Destructor
*/
virtual ~no_extrapolation_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\post dbm has not been modified
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
namespace details {
/*!
\class global_lu_extrapolation_t
\brief Zone extrapolation with global LU clock bounds (abstract class)
*/
class global_lu_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : global LU clock bounds map
*/
global_lu_extrapolation_t(std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
global_lu_extrapolation_t(tchecker::zg::details::global_lu_extrapolation_t const & e) = default;
/*!
\brief Move constructor
*/
global_lu_extrapolation_t(tchecker::zg::details::global_lu_extrapolation_t && e) = default;
/*!
\brief Destructor
*/
virtual ~global_lu_extrapolation_t() = default;
/*!
\brief Assignment operator
*/
tchecker::zg::details::global_lu_extrapolation_t &
operator=(tchecker::zg::details::global_lu_extrapolation_t const & e) = default;
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::global_lu_extrapolation_t & operator=(tchecker::zg::details::global_lu_extrapolation_t && e) = default;
protected:
std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> _clock_bounds; /*!< global LU clock bounds map */
};
} // end of namespace details
/*!
\class global_extra_lu_t
\brief ExtraLU zone extrapolation with global LU clock bounds
*/
class global_extra_lu_t final : public tchecker::zg::details::global_lu_extrapolation_t {
public:
using tchecker::zg::details::global_lu_extrapolation_t::global_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_lu_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU has been applied to dbm with global LU clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class global_extra_lu_plus_t
\brief ExtraLU+ zone extrapolation with global LU clock bounds
*/
class global_extra_lu_plus_t final : public tchecker::zg::details::global_lu_extrapolation_t {
public:
using tchecker::zg::details::global_lu_extrapolation_t::global_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_lu_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU+ has been applied to dbm with global LU clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
namespace details {
/*!
\class local_lu_extrapolation_t
\brief Zone extrapolation with local LU clock bounds (abstract class)
*/
class local_lu_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : local LU clock bounds map
*/
local_lu_extrapolation_t(std::shared_ptr<tchecker::clockbounds::local_lu_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t const & e);
/*!
\brief Move constructor
*/
local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t && e);
/*!
\brief Destructor
*/
virtual ~local_lu_extrapolation_t();
/*!
\brief Assignment operator
*/
tchecker::zg::details::local_lu_extrapolation_t & operator=(tchecker::zg::details::local_lu_extrapolation_t const & e);
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::local_lu_extrapolation_t & operator=(tchecker::zg::details::local_lu_extrapolation_t && e);
protected:
tchecker::clockbounds::map_t * _l; /*!< clock bounds L map */
tchecker::clockbounds::map_t * _u; /*!< clock bounds U map */
std::shared_ptr<tchecker::clockbounds::local_lu_map_t const> _clock_bounds; /*!< local LU clock bounds map */
};
} // end of namespace details
/*!
\class local_extra_lu_t
\brief ExtraLU zone extrapolation with local LU clock bounds
*/
class local_extra_lu_t final : public tchecker::zg::details::local_lu_extrapolation_t {
public:
using tchecker::zg::details::local_lu_extrapolation_t::local_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_lu_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU has been applied to dbm with local LU clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class local_extra_lu_plus_t
\brief ExtraLU+ zone extrapolation with local LU clock bounds
*/
class local_extra_lu_plus_t final : public tchecker::zg::details::local_lu_extrapolation_t {
public:
using tchecker::zg::details::local_lu_extrapolation_t::local_lu_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_lu_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraLU+ has been applied to dbm with local LU clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
namespace details {
/*!
\class global_m_extrapolation_t
\brief Zone extrapolation with global M clock bounds (abstract class)
*/
class global_m_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : global M clock bounds map
*/
global_m_extrapolation_t(std::shared_ptr<tchecker::clockbounds::global_m_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
global_m_extrapolation_t(tchecker::zg::details::global_m_extrapolation_t const & e) = default;
/*!
\brief Move constructor
*/
global_m_extrapolation_t(tchecker::zg::details::global_m_extrapolation_t && e) = default;
/*!
\brief Destructor
*/
virtual ~global_m_extrapolation_t() = default;
/*!
\brief Assignment operator
*/
tchecker::zg::details::global_m_extrapolation_t &
operator=(tchecker::zg::details::global_m_extrapolation_t const & e) = default;
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::global_m_extrapolation_t & operator=(tchecker::zg::details::global_m_extrapolation_t && e) = default;
protected:
std::shared_ptr<tchecker::clockbounds::global_m_map_t const> _clock_bounds; /*!< global LU clock bounds map */
};
} // end of namespace details
/*!
\class global_extra_m_t
\brief ExtraM zone extrapolation with global M clock bounds
*/
class global_extra_m_t final : public tchecker::zg::details::global_m_extrapolation_t {
public:
using tchecker::zg::details::global_m_extrapolation_t::global_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_m_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM has been applied to dbm with global M clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class global_extra_m_plus_t
\brief ExtraM+ zone extrapolation with global M clock bounds
*/
class global_extra_m_plus_t final : public tchecker::zg::details::global_m_extrapolation_t {
public:
using tchecker::zg::details::global_m_extrapolation_t::global_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~global_extra_m_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM+ has been applied to dbm with global M clock bounds
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
namespace details {
/*!
\class local_m_extrapolation_t
\brief Zone extrapolation with local M clock bounds (abstract class)
*/
class local_m_extrapolation_t : public tchecker::zg::extrapolation_t {
public:
/*!
\brief Constructor
\param clock_bounds : local M clock bounds map
*/
local_m_extrapolation_t(std::shared_ptr<tchecker::clockbounds::local_m_map_t const> const & clock_bounds);
/*!
\brief Copy constructor
*/
local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t const & e);
/*!
\brief Move constructor
*/
local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t && e);
/*!
\brief Destructor
*/
virtual ~local_m_extrapolation_t();
/*!
\brief Assignment operator
*/
tchecker::zg::details::local_m_extrapolation_t & operator=(tchecker::zg::details::local_m_extrapolation_t const & e);
/*!
\brief Move-assignment operator
*/
tchecker::zg::details::local_m_extrapolation_t & operator=(tchecker::zg::details::local_m_extrapolation_t && e);
protected:
tchecker::clockbounds::map_t * _m; /*!< clock bounds M map */
std::shared_ptr<tchecker::clockbounds::local_m_map_t const> _clock_bounds; /*!< local M clock bounds map */
};
} // end of namespace details
/*!
\class local_extra_m_t
\brief ExtraM zone extrapolation with local M clock bounds
*/
class local_extra_m_t final : public tchecker::zg::details::local_m_extrapolation_t {
public:
using tchecker::zg::details::local_m_extrapolation_t::local_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_m_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM has been applied to dbm with local M clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\class local_extra_m_plus_t
\brief ExtraM+ zone extrapolation with local M clock bounds
*/
class local_extra_m_plus_t final : public tchecker::zg::details::local_m_extrapolation_t {
public:
using tchecker::zg::details::local_m_extrapolation_t::local_m_extrapolation_t;
/*!
\brief Destructor
*/
virtual ~local_extra_m_plus_t() = default;
/*!
\brief Zone extrapolation
\param dbm : a dbm
\param dim : dimension of dbm
\param vloc : a tuple of locations
\pre dim is 1 plus the number of clocks in the global LU clock bounds map (checked by assertion)
\post ExtraM+ has been applied to dbm with local M clock bounds in vloc
*/
virtual void extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc);
};
/*!
\brief Type of extrapolation
*/
enum extrapolation_type_t {
NO_EXTRAPOLATION, /*!< see tchecker::zg::no_extrapolation_t */
EXTRA_LU_GLOBAL, /*!< see tchecker::zg::global_extra_lu_t */
EXTRA_LU_LOCAL, /*!< see tchecker::zg::local_extra_lu_t */
EXTRA_LU_PLUS_GLOBAL, /*!< see tchecker::zg::global_extra_lu_plus_t */
EXTRA_LU_PLUS_LOCAL, /*!< see tchecker::zg::local_extra_lu_plus_t */
EXTRA_M_GLOBAL, /*!< see tchecker::zg::global_extra_m_t */
EXTRA_M_LOCAL, /*!< see tchecker::zg::local_extra_m_t */
EXTRA_M_PLUS_GLOBAL, /*!< see tchecker::zg::global_extra_m_plus_t */
EXTRA_M_PLUS_LOCAL, /*!< see tchecker::zg::local_extra_m_plus_t */
};
/*!
\brief Zone extrapolation factory
\param extrapolation_type : type of extrapolation
\param system : system of timed processes
\return a zone extrapolation of type extrapolation_type using clock bounds
inferred from system, nullptr if clock bounds cannot be inferred from system (see
tchecker::clockbounds::compute_clockbounds)
\note the returned extrapolation must be deallocated by the caller
\throw std::invalid_argument : if extrapolation_type is unknown
*/
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::ta::system_t const & system);
/*!
\brief Zone extrapolation factory
\param extrapolation_type : type of extrapolation
\param clock_bounds : clock bounds
\return a zone extrapolation of type extrapolation_type using clock bounds from
clock_bounds
\note the returned extrapolation must be deallocated by the caller
\throw std::invalid_argument : if extrapolation_type is unknown
*/
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::clockbounds::clockbounds_t const & clock_bounds);
} // end of namespace zg
} // end of namespace tchecker
#endif // TCHECKER_ZG_EXTRAPOLATION_HH

115
include/tchecker/zg/semantics.hh
View file

@ -8,6 +8,8 @@
#ifndef TCHECKER_ZG_SEMANTICS_HH
#define TCHECKER_ZG_SEMANTICS_HH
#include <memory>
#include "tchecker/basictypes.hh"
#include "tchecker/dbm/db.hh"
#include "tchecker/variables/clocks.hh"
@ -297,12 +299,125 @@ public:
tchecker::clock_constraint_container_t const & tgt_invariant);
};
/*!
\class distinguished_semantics_t
\brief Distinguished semantics: "classic" semantics. A transition is either
* an action transition or a delay transition.
*/
class distinguished_semantics_t final : public tchecker::zg::semantics_t {
public:
/*!
\brief Destructor
*/
virtual ~distinguished_semantics_t() = default;
/*!
\brief Compute initial zone
\param dbm : a DBM
\param dim : dimension of dbm
\param delay_allowed : ignored
\param invariant : invariant
\post dbm is the zone that only contains the zero valuation
\return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise,
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if the zero valuation does not
satisfy invariant.
*/
virtual tchecker::state_status_t initial(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant);
/*!
\brief Compute final zone
\param dbm : a DBM
\param dim : dimension of dbm
\param delay_allowed : true if delay is allowed in final state
\param invariant : invariant
\post dbm is the universal positive zone restricted to invariant
\return STATE_OK if the resulting dbm is not empty. Otherwise,
tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED if the intersection of the
universal positive zone and invariant is empty
*/
virtual tchecker::state_status_t final(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant);
/*!
\brief Compute next zone when epsilon transition is used
\param dbm : a DBM
\param dim : dimension of dbm
\param invariant : invariant of current state
\post dbm has been delayed (if allowed), then intersected with src_invariant,
\return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise,
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant
result in an empty zone
*/
tchecker::state_status_t delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim,
tchecker::clock_constraint_container_t const & invariant);
/*!
\brief Compute next zone when action transition is used
\param dbm : a DBM
\param dim : dimension of dbm
\param src_delay_allowed : ignored (always false in this semantics)
\param src_invariant : invariant in source state
\param guard : transition guard
\param clkreset : transition reset
\param tgt_delay_allowed : ignored (always false in this semantics)
\param tgt_invariant : invariant in target state
\post dbm has been intersected with src_invariant, then intersected with guard, then
reset w.r.t clkreset, then intersected with tgt_invariant
\return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise,
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant
result in an empty zone, tchecker::STATE_CLOCKS_GUARD_VIOLATED if intersection
with guard result in an empty zone,
tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED if intersection with
tgt_invariant result in an empty zone
*/
virtual tchecker::state_status_t next(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant);
/*!
\brief Compute previous zone
\param dbm : a DBM
\param dim : dimension of dbm
\param src_delay_allowed : true if delay allowed in source state
\param src_invariant : invariant in source state
\param guard : transition guard
\param clkreset : transition reset
\param tgt_delay_allowed : true if delay allowed in target state
\param tgt_invariant : invariant in target state
\post dbm has been intersected with target invariant and with resets, then reset
clocks have been freed, then the resulting zone has been intersected with guard and
source invariant, then opened down if delay is allowed and intersected with source
invariant again
\return STATE_OK if the resulting dbm is not empty,
tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED is intersection with tgt_invariant
resulted in empty zone,
tchecker::STATE_CLOCKS_RESET_FAILED if intersection with clkreset (as constraints)
resulted in empty zone
tchecker::STATE_CLOCKS_GUARD_VIOLATED if intersection with guard resulted in
empty zone
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant
resulted in empty zone
*/
virtual tchecker::state_status_t prev(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant);
};
/*!
\brief type of semantics
*/
enum semantics_type_t {
STANDARD_SEMANTICS, /*!< see tchecker::zg::standard_semantics_t */
ELAPSED_SEMANTICS, /*!< see tchecker::zg::elapsed_semantics_t */
DISTINGUISHED_SEMANTICS, /*!< see tchecker::zg::distinguished_semantics_t */
};
/*!

315
include/tchecker/zg/state_template.hh Normal file
View file

@ -0,0 +1,315 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_STATE_TEMPLATE_HH
#define TCHECKER_ZG_STATE_TEMPLATE_HH
#if BOOST_VERSION <= 106600
#include <boost/functional/hash.hpp>
#else
#include <boost/container_hash/hash.hpp>
#endif
#include "tchecker/ta/state.hh"
#include "tchecker/utils/shared_objects.hh"
#include "tchecker/clockbounds/clockbounds.hh"
/*!
\file state_template.hh
\brief State of a zone graph
*/
namespace tchecker {
namespace zg {
/*!
\brief Type of shared zone, DBM implementation
*/
template<typename Tused_zone_t>
using shared_zone_helper_t = tchecker::make_shared_t<Tused_zone_t>;
/*!
\brief Type of shared pointer to zone, DBM implementation
*/
template<typename Tused_zone_t>
using zone_sptr_helper_t = tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t>>;
/*!
\class state_help_t
\brief state of a zone graph
\note to instantiate a symbolic state of a usual zg, set
* zone_t = tchecker::zg::zone_t
* to instatiate a symbolic state of a vcg, set
* zone_t = tchecker::vcg::zone_t
*/
template<typename Tused_zone_t>
class state_help_t : public tchecker::ta::state_t {
public:
/*!
\brief Constructor
\param vloc : tuple of locations
\param intval : integer variables valuation
\param zone : zone of clock valuations
\pre vloc, intval and zone must not point to nullptr (checked by assertion)
*/
explicit state_help_t(tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t>> const & zone)
: tchecker::ta::state_t(vloc, intval), _zone(zone)
{
assert(_zone.ptr() != nullptr);
}
/*!
\brief Partial copy constructor
\param state : a state
\param vloc : tuple of locations
\param intval : integer variables valuation
\param zone : zone of clock valuations
\pre vloc, intval and zone must not point to nullptr (checked by assertion)
\note the state is copied from s, except the tuple of locations which is
initialized from vloc, and the valuation of bounded integer variables which
is initialized from intval, and the zone which is initialized from zone
*/
state_help_t(tchecker::ta::state_t const & s, tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t>> const & zone)
: tchecker::ta::state_t(s, vloc, intval), _zone(zone)
{
assert(_zone.ptr() != nullptr);
}
/*!
\brief Copy constructor (deleted)
*/
state_help_t(state_help_t const &) = delete;
/*!
\brief Move constructor (deleted)
*/
state_help_t(state_help_t &&) = delete;
/*!
\brief Destructor
*/
~state_help_t() = default;
/*!
\brief Assignment operator (deleted)
*/
tchecker::zg::state_help_t<Tused_zone_t> & operator=(tchecker::zg::state_help_t<Tused_zone_t> const &) = default;
/*!
\brief Move-assignment operator (deleted)
*/
tchecker::zg::state_help_t<Tused_zone_t> & operator=(tchecker::zg::state_help_t<Tused_zone_t> &&) = default;
/*!
\brief Accessor
\return zone in this state
*/
constexpr inline Tused_zone_t const & zone() const { return *_zone; }
/*!
\brief Accessor
\return reference to pointer to the zone in this state
*/
inline tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t>> & zone_ptr() { return _zone; }
/*!
\brief Accessor
\return pointer to const zone in this state
*/
inline tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t> const> zone_ptr() const
{
return tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t> const>(_zone.ptr());
}
private:
tchecker::intrusive_shared_ptr_t<shared_zone_helper_t<Tused_zone_t> > _zone; /*!< Zone over clock valuations */
};
/*!
\brief Equality check
\param s1 : state
\param s2 : state
\return true if s1 and s2 have same zone, same tuple of locations and same
valuation of bounded integer variables, false otherwise
*/
template<typename Tused_zone_t>
bool operator==(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2)
{
return tchecker::ta::operator==(s1, s2) && (s1.zone() == s2.zone());
}
/*!
\brief Disequality check
\param s1 : state
\param s2 : state
\return true if s1 and s2 have different zones, or different tuples of locations or different valuations of bounded integer
variables, false otherwise
*/
template<typename Tused_zone_t>
bool operator!=(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2)
{
return !(s1 == s2);
}
/*!
\brief Equality check for shared states
\param s1 : state
\param s2 : state
\return true if s1 and s2 have same zone, same tuple of locations and same
valuation of bounded integer variables, false otherwise
\note this should only be used on states that have shared internal components: this
function checks pointer equality (not values equality)
*/
template<typename Tused_zone_t>
bool shared_equal_to(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2)
{
return tchecker::ta::shared_equal_to(s1, s2) && (s1.zone_ptr() == s2.zone_ptr());
}
/*!
\brief Covering check
\param s1 : state
\param s2 : state
\return true if s1 and s2 have the same tuple of locations and integer
variables valuation, and the zone in s1 is included in the zone in s2, false
otherwise
*/
template<typename Tused_zone_t>
bool operator<=(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2)
{
return tchecker::ta::operator==(s1, s2) && (s1.zone() <= s2.zone());
}
/*!
\brief Covering check for shared states
\param s1 : state
\param s2 : state
\return true if s1 and s2 have the same tuple of locations and integer
variables valuation, and the zone in s1 is included in the zone in s2, false
otherwise
\note this should only be used on states that have shared internal components: this
function checks pointers instead of values when relevant
*/
template<typename Tused_zone_t>
bool shared_is_le(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2)
{
return tchecker::ta::shared_equal_to(s1, s2) && (s1.zone_ptr() == s2.zone_ptr() || s1.zone() <= s2.zone());
}
/*!
\brief aLU subsumption check
\param s1 : state
\param s2 : state
\param l : clock lower bounds
\param u : clock upper bounds
\return true if s1 and s2 have the same tuple of locations and integer
variables valuation, and the zone in s1 is included in aLU-abstraction of the
zone in s2, false otherwise
\note this should only be used on states that have shared internal components: this
function checks pointers instead of values when relevant
*/
template<typename Tused_zone_t>
bool is_alu_le(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2, tchecker::clockbounds::map_t const & l,
tchecker::clockbounds::map_t const & u)
{
return tchecker::ta::operator==(s1, s2) && s1.zone().is_alu_le(s2.zone(), l, u);
}
/*!
\brief aLU subsumption check for shared states
\param s1 : state
\param s2 : state
\param l : clock lower bounds
\param u : clock upper bounds
\return true if s1 and s2 have the same tuple of locations and integer
variables valuation, and the zone in s1 is included in aLU-abstraction of the
zone in s2, false otherwise
\note this should only be used on states that have shared internal components: this
function checks pointers instead of values when relevant
*/
template<typename Tused_zone_t>
bool shared_is_alu_le(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2,
tchecker::clockbounds::map_t const & l, tchecker::clockbounds::map_t const & u)
{
return tchecker::ta::shared_equal_to(s1, s2) && (s1.zone_ptr() == s2.zone_ptr() || s1.zone().is_alu_le(s2.zone(), l, u));
}
/*!
\brief Hash
\param s : state
\return Hash value for state s
*/
template<typename Tused_zone_t>
std::size_t hash_value(tchecker::zg::state_help_t<Tused_zone_t> const & s)
{
std::size_t h = tchecker::ta::hash_value(s);
boost::hash_combine(h, s.zone());
return h;
}
/*!
\brief Hash for shared states
\param s : state
\return Hash value for state s
\note this should only be used on states that have shared internal components: this function
hashes the pointers (not the values)
*/
template<typename Tused_zone_t>
std::size_t shared_hash_value(tchecker::zg::state_help_t<Tused_zone_t> const & s)
{
std::size_t h = tchecker::ta::shared_hash_value(s);
boost::hash_combine(h, s.zone_ptr());
return h;
}
/*!
\brief Lexical ordering on states of the zone graph
\param s1 : a state
\param s2 : a state
\return 0 if s1 and s2 are equal, a negative value if s1 is smaller than s2
w.r.t. lexical ordering on zone,tuple of locations and valuation of bounded
integer variables, a positive value otherwise
*/
template<typename Tused_zone_t>
int lexical_cmp(tchecker::zg::state_help_t<Tused_zone_t> const & s1, tchecker::zg::state_help_t<Tused_zone_t> const & s2)
{
int ta_cmp = tchecker::ta::lexical_cmp(s1, s2);
if (ta_cmp != 0)
return ta_cmp;
return s1.zone().lexical_cmp(s2.zone());
}
/*!
\brief Type of shared state
*/
template<typename Tused_zone_t>
using shared_state_help_t = tchecker::make_shared_t<tchecker::zg::state_help_t<Tused_zone_t>>;
/*!
\brief Type of pointer to shared state
*/
template<typename Tused_zone_t>
using state_sptr_help_t = tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_state_help_t<Tused_zone_t>>;
/*!
\brief Type of pointer to shared const state
*/
template<typename Tused_zone_t>
using const_state_sptr_help_t = tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_state_help_t<Tused_zone_t> const>;
} // end of namespace zg
} // end of namepsace tchecker
#endif

598
include/tchecker/zg/zg.hh
View file

@ -8,28 +8,13 @@
#ifndef TCHECKER_ZG_HH
#define TCHECKER_ZG_HH
#include <cstdlib>
#include "tchecker/basictypes.hh"
#include "tchecker/clockbounds/clockbounds.hh"
#include "tchecker/syncprod/vedge.hh"
#include "tchecker/syncprod/vloc.hh"
#include "tchecker/ta/system.hh"
#include "tchecker/extrapolation/extrapolation.hh"
#include "tchecker/extrapolation/extrapolation_factory.hh"
#include "tchecker/ta/ta.hh"
#include "tchecker/ts/builder.hh"
#include "tchecker/ts/bwd.hh"
#include "tchecker/ts/fwd.hh"
#include "tchecker/ts/inspector.hh"
#include "tchecker/ts/sharing.hh"
#include "tchecker/utils/shared_objects.hh"
#include "tchecker/variables/clocks.hh"
#include "tchecker/variables/intvars.hh"
#include "tchecker/ts/bwd.hh"
#include "tchecker/zg/allocators.hh"
#include "tchecker/zg/extrapolation.hh"
#include "tchecker/zg/semantics.hh"
#include "tchecker/zg/state.hh"
#include "tchecker/zg/transition.hh"
#include "tchecker/zg/zone.hh"
/*!
\file zg.hh
@ -52,78 +37,11 @@ using initial_iterator_t = tchecker::ta::initial_iterator_t;
*/
using initial_range_t = tchecker::ta::initial_range_t;
/*!
\brief Accessor to initial edges
\param system : a system
\return initial edges
*/
inline tchecker::zg::initial_range_t initial_edges(tchecker::ta::system_t const & system)
{
return tchecker::ta::initial_edges(system);
}
/*!
\brief Dereference type for iterator over initial states
*/
using initial_value_t = tchecker::ta::initial_value_t;
// Initial states
/*!
\brief Compute initial state
\param system : a system
\param vloc : tuple of locations
\param intval : valuation of bounded integer variables
\param zone : a DBM zone
\param vedge : tuple of edges
\param invariant : clock constraint container for initial state invariant
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param initial_range : range of initial state valuations
\pre the size of vloc and vedge is equal to the size of initial_range.
initial_range has been obtained from system.
initial_range yields the initial locations of all the processes ordered by increasing process identifier
\post vloc has been initialized to the tuple of initial locations in initial_range,
intval has been initialized to the initial valuation of bounded integer variables,
vedge has been initialized to an empty tuple of edges.
clock constraints from initial_range invariant have been aded to invariant
zone has been initialized to the initial set of clock valuations according to
semantics and extrapolation.
\return tchecker::STATE_OK if initialization succeeded,
tchecker::STATE_INTVARS_SRC_INVARIANT_VIOLATED if the initial valuation of integer
variables does not satisfy invariant
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if the initial zone is empty
\throw std::runtime_error : if evaluation of invariant throws an exception
*/
tchecker::state_status_t initial(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation,
tchecker::zg::initial_value_t const & initial_range);
/*!
\brief Compute initial state and transition
\param system : a system
\param s : state
\param t : transition
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param v : initial iterator value
\post s has been initialized from v, and t is an empty transition
\return tchecker::STATE_OK if initialization of s and t succeeded, see
tchecker::zg::initial for returned values when initialization fails
\throw std::invalid_argument : if s and v have incompatible sizes
*/
inline tchecker::state_status_t initial(tchecker::ta::system_t const & system, tchecker::zg::state_t & s,
tchecker::zg::transition_t & t, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation, tchecker::zg::initial_value_t const & v)
{
return tchecker::zg::initial(system, s.vloc_ptr(), s.intval_ptr(), s.zone_ptr(), t.vedge_ptr(), t.src_invariant_container(),
semantics, extrapolation, v);
}
// Final edges
@ -140,79 +58,11 @@ using final_iterator_t = tchecker::ta::final_iterator_t;
*/
using final_range_t = tchecker::ta::final_range_t;
/*!
\brief Accessor to final edges
\param system : a system
\param labels : a set of labels
\return range of final edges, i.e. edges to tuple of locations that match labels
*/
inline tchecker::zg::final_range_t final_edges(tchecker::ta::system_t const & system, boost::dynamic_bitset<> const & labels)
{
return tchecker::ta::final_edges(system, labels);
}
/*!
\brief Dereference type for iterator over final edges
*/
using final_value_t = tchecker::ta::final_value_t;
// Final states
/*!
\brief Compute final state
\param system : a system
\param vloc : tuple of locations
\param intval : valuation of bounded integer variables
\param zone : a DBM zone
\param vedge : tuple of edges
\param invariant : clock constraint container for initial state invariant
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param final_range : range of final edges value
\pre the size of vloc and vedge is equal to the size of final_range.
final_range has been obtained from system.
final_range yields a final location to all the processes ordered by increasing process identifier
\post vloc has been initialized to the tuple locations in final_range,
intval has been initialized to the valuation of bounded integer variables in final_range.
vedge has been initialized to an empty tuple of edges.
clock constraints from final_range invariant have been aded to invariant
zone has been initialized to the final set of clock valuations according to
semantics and extrapolation.
\return tchecker::STATE_OK if computation succeeded,
tchecker::STATE_INTVARS_TGT_INVARIANT_VIOLATED if the valuation of integer variables
does not satisfy invariant
tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED if the final zone is empty
\throw std::runtime_error : if evaluation of invariant throws an exception
*/
tchecker::state_status_t final(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation, tchecker::zg::final_value_t const & final_range);
/*!
\brief Compute final state and transition
\param system : a system
\param s : state
\param t : transition
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param v : final iterator value
\post s has been initialized from v, and t is an empty transition
\return tchecker::STATE_OK if initialization of s and t succeeded, see
tchecker::zg::final for returned values when computation fails
\throw std::invalid_argument : if s and v have incompatible sizes
*/
inline tchecker::state_status_t final(tchecker::ta::system_t const & system, tchecker::zg::state_t & s,
tchecker::zg::transition_t & t, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation, tchecker::zg::final_value_t const & v)
{
return tchecker::zg::final(system, s.vloc_ptr(), s.intval_ptr(), s.zone_ptr(), t.vedge_ptr(), t.src_invariant_container(),
semantics, extrapolation, v);
}
// Outgoing edges
/*!
@ -225,115 +75,11 @@ using outgoing_edges_iterator_t = tchecker::ta::outgoing_edges_iterator_t;
*/
using outgoing_edges_range_t = tchecker::ta::outgoing_edges_range_t;
/*!
\brief Accessor to outgoing edges
\param system : a system
\param vloc : tuple of locations
\return range of outgoing synchronized and asynchronous edges from vloc in system
*/
inline tchecker::zg::outgoing_edges_range_t
outgoing_edges(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t const> const & vloc)
{
return tchecker::ta::outgoing_edges(system, vloc);
}
/*!
\brief Type of outgoing vedge (range of synchronized/asynchronous edges)
*/
using outgoing_edges_value_t = tchecker::ta::outgoing_edges_value_t;
// Next states
/*!
\brief Compute next state
\param system : a system
\param vloc : tuple of locations
\param intval : valuation of bounded integer variables
\param zone : a DBM zone
\param vedge : tuple of edges
\param src_invariant : clock constraint container for invariant of vloc before
it is updated
\param guard : clock constraint container for guard of vedge
\param reset : clock resets container for clock resets of vedge
\param tgt_invariant : clock constaint container for invariant of vloc after it
is updated
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param edges : tuple of edge from vloc (range of synchronized/asynchronous edges)
\pre the source location in edges match the locations in vloc.
No process has more than one edge in edges.
The pid of every process in edges is less than the size of vloc
\post the locations in vloc have been updated to target locations of the
processes involved in edges, and they have been left unchanged for the other
processes.
The values of variables in intval have been updated according to the statements
in edges.
Clock constraints from the invariants of vloc before it is updated have been
pushed to src_invariant.
Clock constraints from the guards in edges have been pushed into guard.
Clock resets from the statements in edges have been pushed into reset.
Clock constraints from the invariants in the updated vloc have been pushed
into tgt_invariant.
The zone has been updated according to semantics and extrapolation from
src_invariant, guard, reset, tgt_invariant (and delay)
\return tchecker::STATE_OK if state computation succeeded,
tchecker::STATE_INCOMPATIBLE_EDGE if the source locations in edges do not match
vloc,
tchecker::STATE_INTVARS_SRC_INVARIANT_VIOLATED if the valuation intval does not
satisfy the invariant in vloc,
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if the zone does not satisfy the
invariant in vloc
tchecker::STATE_INTVARS_GUARD_VIOLATED if the values in intval do not satisfy
the guard of edges,
tchecker::STATE_CLOCKS_GUARD_VIOLATED if the zone updated w.r.t. src_invariant
does not satisfy the guard of the edges
tchecker::STATE_INTVARS_STATEMENT_FAILED if statements in edges cannot be
applied to intval
tchecker::STATE_INTVARS_TGT_INVARIANT_VIOLATED if the updated intval does not
satisfy the invariant of updated vloc.
tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED if the updated zone does not
satisfy the invariant of updated vloc
\throw std::invalid_argument : if a pid in edges is greater or equal to the
size of vloc
\throw std::runtime_error : if the guard in edges generates clock resets, or if
the statements in edges generate clock constraints, or if the invariant in
updated vloc generates clock resets
\throw std::runtime_error : if evaluation of invariants, guards or statements
throws an exception
*/
tchecker::state_status_t next(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & src_invariant,
tchecker::clock_constraint_container_t & guard, tchecker::clock_reset_container_t & reset,
tchecker::clock_constraint_container_t & tgt_invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation,
tchecker::zg::outgoing_edges_value_t const & edges);
/*!
\brief Compute next state and transition
\param system : a system
\param s : state
\param t : transition
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param v : outgoing edge value
\post s have been updated from v according to semantics and extrapolation, and
t is the set of edges in v
\return status of state s after update (see tchecker::zg::next)
\throw std::invalid_argument : if s and v have incompatible size
*/
inline tchecker::state_status_t next(tchecker::ta::system_t const & system, tchecker::zg::state_t & s,
tchecker::zg::transition_t & t, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation,
tchecker::zg::outgoing_edges_value_t const & v)
{
return tchecker::zg::next(system, s.vloc_ptr(), s.intval_ptr(), s.zone_ptr(), t.vedge_ptr(), t.src_invariant_container(),
t.guard_container(), t.reset_container(), t.tgt_invariant_container(), semantics, extrapolation, v);
}
// Incoming edges
@ -350,243 +96,18 @@ using incoming_edges_iterator_t = tchecker::ta::incoming_edges_iterator_t;
*/
using incoming_edges_range_t = tchecker::ta::incoming_edges_range_t;
/*!
\brief Accessor to incoming edges
\param system : a system
\param vloc : tuple of locations
\return range of incoming synchronized and asynchronous edges to vloc in system
*/
inline tchecker::zg::incoming_edges_range_t
incoming_edges(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t const> const & vloc)
{
return tchecker::ta::incoming_edges(system, vloc);
}
/*!
\brief Type of incoming tuple of edges (range of synchronized/asynchronous edges)
*/
using incoming_edges_value_t = tchecker::ta::incoming_edges_value_t;
// Previous states
/*!
\brief Compute previous state
\param system : a system
\param vloc : tuple of locations
\param intval : valuation of bounded integer variables
\param zone : a DBM zone
\param vedge : tuple of edges
\param src_invariant : clock constraint container for source invariant
\param guard : clock constraint container for guard of vedge
\param reset : clock resets container for clock resets of vedge
\param tgt_invariant : clock constaint container for target invariant
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param edges : tuple of incoming edges to vloc (range of synchronized/asynchronous edges)
\pre the target locations in edges match the locations in vloc.
No process has more than one edge in edges.
The pid of every process in edges is less than the size of vloc
\post the locations in vloc have been updated to source locations of the
processes involved in edges, and they have been left unchanged for the other
processes.
The values of variables in intval have been updated according to the statements
in edges.
Clock constraints from the source invariant have been pushed to src_invariant.
Clock constraints from the guards in edges have been pushed into guard.
Clock resets from the statements in edges have been pushed into reset.
Clock constraints from the target invariants have been pushed into tgt_invariant.
The zone has been updated according to semantics and extrapolation from
src_invariant, guard, reset, tgt_invariant (and delay)
\return tchecker::STATE_OK if state computation succeeded,
tchecker::STATE_INCOMPATIBLE_EDGE if the target locations in edges do not match
vloc or if the bounded integer variables valuation in edges does not transform into
intval going through edges,
tchecker::STATE_INTVARS_SRC_INVARIANT_VIOLATED if the updated intval does not satisfy
the source invariant
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if the updated zone does not satisfy the
source invariant,
tchecker::STATE_INTVARS_GUARD_VIOLATED if the updated intval do not satisfy the guard
of edges,
tchecker::STATE_CLOCKS_GUARD_VIOLATED if the updated zone does not satisfy the guard
of the edges
tchecker::STATE_INTVARS_STATEMENT_FAILED if statements in edges cannot be
applied to intval
tchecker::STATE_INTVARS_TGT_INVARIANT_VIOLATED if intval does not satisfy the target
invariant
tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED if the zone does not satisfy the target
invariant
\throw std::invalid_argument : if a pid in edges is greater or equal to the
size of vloc
\throw std::runtime_error : if the guard in edges generates clock resets, or if
the statements in edges generate clock constraints, or if the invariant in
updated vloc generates clock resets
\throw std::runtime_error : if evaluation of invariants, guards or statements
throws an exception
*/
tchecker::state_status_t prev(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & src_invariant,
tchecker::clock_constraint_container_t & guard, tchecker::clock_reset_container_t & reset,
tchecker::clock_constraint_container_t & tgt_invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation,
tchecker::zg::incoming_edges_value_t const & edges);
/*!
\brief Compute previous state and transition
\param system : a system
\param s : state
\param t : transition
\param semantics : a zone semantics
\param extrapolation : an extrapolation
\param v : incoming edge value
\post s have been updated from v according to semantics and extrapolation, and
t is the set of edges in v
\return status of state s after update (see tchecker::zg::prev)
\throw std::invalid_argument : if s and v have incompatible size
*/
inline tchecker::state_status_t prev(tchecker::ta::system_t const & system, tchecker::zg::state_t & s,
tchecker::zg::transition_t & t, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation,
tchecker::zg::incoming_edges_value_t const & v)
{
return tchecker::zg::prev(system, s.vloc_ptr(), s.intval_ptr(), s.zone_ptr(), t.vedge_ptr(), t.src_invariant_container(),
t.guard_container(), t.reset_container(), t.tgt_invariant_container(), semantics, extrapolation, v);
}
// Inspector
/*!
\brief Computes the set of labels of a state
\param system : a system
\param s : a state
\return the set of labels on state s
*/
boost::dynamic_bitset<> labels(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s);
/*!
\brief Checks is a state is a valid final state
\param system : a system
\param s : a state
\return true if s has a non-empty zone, false otherwise
*/
bool is_valid_final(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s);
/*!
\brief Checks if a zone contains an initial valuation
\param system : a system
\param zone : a DBM zone
\pre the dimension of zone corresponds to the number of flattened clock variables
in system plus one (checked by assertion)
\return true if zone contains the initial valuation where all clocks are equal to zero,
false otherwise
*/
bool is_initial(tchecker::ta::system_t const & system, tchecker::zg::zone_t const & zone);
/*!
\brief Checks if a state is initial
\param system : a system
\param s : a state
\pre s is a state computed from system
\return true if s is an initial state in system, false otherwise
*/
bool is_initial(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s);
// Attributes
/*!
\brief Accessor to state attributes as strings
\param system : a system
\param s : a state
\param m : a map of string pairs (key, value)
\post the tuple of locations, the integer variables valuation and the zone in
s have been added to map m
*/
void attributes(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s, std::map<std::string, std::string> & m);
/*!
\brief Accessor to transition attributes as strings
\param system : a system
\param t : a transition
\param m : a map of string pairs (key, value)
\post the tuple of edges in t has been added to map m
*/
void attributes(tchecker::ta::system_t const & system, tchecker::zg::transition_t const & t,
std::map<std::string, std::string> & m);
// Initialize
/*!
\brief Initialization from attributes
\param system : a system
\param vloc : a vector of locations
\param intval : valuation of bounded integer variables
\param zone : a DBM zone
\param vedge : a vector of edges
\param invariant : clock constraint container for state invariant
\param attributes : map of attributes
\pre attributes["vloc"] is defined and follows the syntax required by function
tchecker::from_string(tchecker::vloc_t &, tchecker::system::system_t const &, std::string const &);
attributes["inval"] is defined and follows the syntax required by function
tchecker::from_string(tchecker::intval_t &, tchecker::system::system_t const &, std::string const &);
attributes["zone"] is defined and follows the syntax required by function
tchecker::from_string(tchecker::clock_constraint_container_t &, tchecker::clock_variables_t const &,
std::string const &);
\post vloc has been initialized from attributes["vloc"]
intval has been initialized from attributes["intval"]
zone has been initialized from attributes["zone"] and invariant
vedge has been initialized to the empty vector of edges
and invariant contains the invariant in vloc
\return tchecker::STATE_OK if initialization succeeded
tchecker::STATE_BAD if initialization failed
tchecker::STATE_INTVARS_SRC_INVARIANT_VIOLATED if attributes["intval"] does not satisfy the invariant in
vloc
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if attributes["zone"] intersected with the invariant in
vloc is empty
*/
tchecker::state_status_t initialize(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & invariant,
std::map<std::string, std::string> const & attributes);
/*!
\brief Initialization from attributes
\param system : a system
\param s : state
\param t : transition
\param attributes : map of attributes
\post s and t have been initialized from attributes["vloc"], attributes["intval"] and attributes["zone"]
the src invariant container in t contains the invariant of state s
\return tchecker::STATE_OK if initialization succeeded
tchecker::STATE_BAD otherwise
tchecker::STATE_INTVARS_SRC_INVARIANT_VIOLATED if attributes["intval"] does not satisfy the invariant in
attributes["vloc"]
tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if attributes["zone"] intersected with the invariant in
vloc is empty
*/
inline tchecker::state_status_t initialize(tchecker::ta::system_t const & system, tchecker::zg::state_t & s,
tchecker::zg::transition_t & t,
std::map<std::string, std::string> const & attributes)
{
return tchecker::zg::initialize(system, s.vloc_ptr(), s.intval_ptr(), s.zone_ptr(), t.vedge_ptr(),
t.src_invariant_container(), attributes);
}
// zg_t
/*!
\class zg_t
\class zg_helper_t
\brief Transition system of the zone graph over system of timed processes with
state and transition allocation
\note all returned states and transitions are deallocated automatically
*/
class zg_t final : public tchecker::ts::fwd_t<tchecker::zg::state_sptr_t, tchecker::zg::const_state_sptr_t,
class zg_t : public tchecker::ts::fwd_t<tchecker::zg::state_sptr_t, tchecker::zg::const_state_sptr_t,
tchecker::zg::transition_sptr_t, tchecker::zg::const_transition_sptr_t>,
public tchecker::ts::bwd_t<tchecker::zg::state_sptr_t, tchecker::zg::const_state_sptr_t,
tchecker::zg::transition_sptr_t, tchecker::zg::const_transition_sptr_t>,
@ -620,6 +141,7 @@ public:
using inspector_t = tchecker::ts::inspector_t<tchecker::zg::const_state_sptr_t, tchecker::zg::const_transition_sptr_t>;
using sharing_t = tchecker::ts::sharing_t<tchecker::zg::state_sptr_t, tchecker::zg::transition_sptr_t>;
using sst_t = fwd_t::sst_t;
using state_t = fwd_t::state_t;
using const_state_t = fwd_t::const_state_t;
@ -634,6 +156,7 @@ public:
using incoming_edges_range_t = bwd_impl_t::incoming_edges_range_t;
using incoming_edges_value_t = bwd_impl_t::incoming_edges_value_t;
/*!
\brief Constructor
\param system : a system of timed processes
@ -646,17 +169,24 @@ public:
*/
zg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
std::shared_ptr<tchecker::zg::semantics_t> const & semantics,
std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size);
std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size)
: _system(system), _sharing_type(sharing_type), _semantics(semantics), _extrapolation(extrapolation),
_state_allocator(block_size, block_size, _system->processes_count(), block_size,
_system->intvars_count(tchecker::VK_FLATTENED), block_size,
_system->clocks_count(tchecker::VK_FLATTENED) + 1, table_size),
_transition_allocator(block_size, block_size, _system->processes_count(), table_size)
{
}
/*!
\brief Copy constructor (deleted)
*/
zg_t(tchecker::zg::zg_t const &) = delete;
zg_t(zg_t const &) = delete;
/*!
\brief Move constructor (deleted)
*/
zg_t(tchecker::zg::zg_t &&) = delete;
zg_t(zg_t &&) = delete;
/*!
\brief Destructor
@ -666,12 +196,12 @@ public:
/*!
\brief Assignment operator (deleted)
*/
tchecker::zg::zg_t & operator=(tchecker::zg::zg_t const &) = delete;
zg_t & operator=(zg_t const &) = delete;
/*!
\brief Move-assignment operator (deleted)
*/
tchecker::zg::zg_t & operator=(tchecker::zg::zg_t &&) = delete;
zg_t & operator=(zg_t &&) = delete;
using fwd_t::state;
using fwd_t::status;
@ -731,6 +261,7 @@ public:
virtual void next(tchecker::zg::const_state_sptr_t const & s, outgoing_edges_value_t const & out_edge, std::vector<sst_t> & v,
tchecker::state_status_t mask = tchecker::STATE_OK);
/*!
\brief Next states and transitions with selected status
\param s : state
@ -859,6 +390,7 @@ public:
void split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_constraint_t const & c,
std::vector<tchecker::zg::state_sptr_t> & v);
/*!
\brief Split a state according to a list of clock constraints
\param s : state
@ -870,6 +402,7 @@ public:
void split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_constraint_container_t const & constraints,
std::vector<tchecker::zg::state_sptr_t> & v);
// Inspector
/*!
@ -945,7 +478,41 @@ public:
*/
inline enum tchecker::ts::sharing_type_t sharing_type() const { return _sharing_type; }
/*!
\brief Accessor
\return number of clocks
*/
inline tchecker::clock_id_t clocks_count() { return _system->clocks_count(tchecker::VK_FLATTENED); }
private:
/*!
\brief High-Order function to shorten the handling of states and transitions
\param edge : the parameter for the ta function
\param v : container
\param mask : mask on states
\param ta_func : the function regarding the TA
\param se_func : the function regarding the semantics
\param to_clone : the state to clone (if clone is false, this can be nullptr. otherwise it cant)
\param clone : whether to_clone should be cloned or a new state shall be used
\post the new sst was added to v
*/
template<typename edge_t, typename helping_hand_t>
void sst_handler( edge_t edge, std::vector<sst_t> & v, tchecker::state_status_t mask,
tchecker::state_status_t (*ta_func)(tchecker::ta::system_t const &,
tchecker::zg::state_sptr_t &,
tchecker::zg::transition_sptr_t &,
edge_t &,
helping_hand_t *),
tchecker::state_status_t (*se_func)( tchecker::ta::system_t const &,
tchecker::zg::semantics_t &,
tchecker::dbm::db_t *,
tchecker::clock_id_t,
tchecker::zg::state_sptr_t &,
tchecker::zg::transition_sptr_t &,
helping_hand_t *),
tchecker::zg::const_state_sptr_t const & to_clone, bool clone
);
/*!
\brief Clone and constrain a state
\param s : a state
@ -955,6 +522,15 @@ private:
tchecker::zg::state_sptr_t clone_and_constrain(tchecker::zg::const_state_sptr_t const & s,
tchecker::clock_constraint_t const & c);
/*!
\brief Clone and constrain a state
\param s : a state
\param c : a vector of clock constraints
\return a clone of s with its zone intersected with c
*/
tchecker::zg::state_sptr_t clone_and_constrain(tchecker::zg::const_state_sptr_t const & s,
clock_constraint_container_t const & c);
std::shared_ptr<tchecker::ta::system_t const> _system; /*!< System of timed processes */
enum tchecker::ts::sharing_type_t _sharing_type; /*!< Sharing of state/transition components */
std::shared_ptr<tchecker::zg::semantics_t> _semantics; /*!< Zone semantics */
@ -963,6 +539,8 @@ private:
tchecker::zg::transition_pool_allocator_t _transition_allocator; /*! Pool allocator of transitions */
};
/* tools */
/*!
\brief Compute initial state of a zone graph from a tuple of locations
\param zg : zone graph
@ -971,8 +549,9 @@ private:
\return the initial state of zg with tuple of locations vloc and status
compatible with mask if any, nullptr otherwise
*/
tchecker::zg::state_sptr_t initial(tchecker::zg::zg_t & zg, tchecker::vloc_t const & vloc,
tchecker::state_status_t mask = tchecker::STATE_OK);
tchecker::zg::state_sptr_t
initial(tchecker::zg::zg_t& zg,
tchecker::vloc_t const & vloc, tchecker::state_status_t mask = tchecker::STATE_OK);
/*!
\brief Compute next state and transition from a tuple of edges
@ -984,42 +563,17 @@ tchecker::zg::state_sptr_t initial(tchecker::zg::zg_t & zg, tchecker::vloc_t con
along tuple of edges vedge if any, (nullptr, nullptr) otherwise
*/
std::tuple<tchecker::zg::state_sptr_t, tchecker::zg::transition_sptr_t>
next(tchecker::zg::zg_t & zg, tchecker::zg::const_state_sptr_t const & s, tchecker::vedge_t const & vedge,
tchecker::state_status_t mask = tchecker::STATE_OK);
next(tchecker::zg::zg_t &zg,
tchecker::zg::const_state_sptr_t const & s, tchecker::vedge_t const & vedge, tchecker::state_status_t mask = tchecker::STATE_OK);
/*!
\brief Factory of zone graphs with clock bounds computed from system
\param system : system of timed processes
\param sharing_type : type of sharing
\param semantics_type : type of zone semantics
\param extrapolation_type : type of zone extrapolation
\param block_size : number of objects allocated in a block
\param table_size : size of hash tables
\return a zone graph over system with zone semantics and zone extrapolation
defined from semantics_type and extrapolation_type, and allocation of
block_size objects at a time, nullptr if clock bounds cannot be inferred from
system
*/
tchecker::zg::zg_t * factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
/* factory */
std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size,
std::size_t table_size);
/*!
\brief Factory of zone graphs with given clock bounds
\param system : system of timed processes
\param sharing_type : type of sharing
\param semantics_type : type of zone semantics
\param extrapolation_type : type of zone extrapolation
\param clock_bounds : clock bounds
\param block_size : number of objects allocated in a block
\param table_size : size of hash tables
\return a zone graph over system with zone semantics and zone extrapolation
defined from semantics_type, extrapolation_type and clock_bounds, and allocation
of block_size objects at a time, nullptr if clock bounds cannot be inferred from
system
*/
tchecker::zg::zg_t * factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
enum tchecker::zg::extrapolation_type_t extrapolation_type,
tchecker::clockbounds::clockbounds_t const & clock_bounds, std::size_t block_size,

18
include/tchecker/zg/zone.hh
View file

@ -32,6 +32,9 @@ namespace zg {
*/
class zone_t : public tchecker::cached_object_t {
public:
/*!
\brief Assignment operator
\param zone : a DBM zone
@ -119,7 +122,7 @@ public:
\brief Accessor
\return dimension of the zone
*/
inline std::size_t dim() const { return _dim; }
inline tchecker::clock_id_t dim() const { return _dim; }
/*!
\brief Output
@ -311,6 +314,19 @@ template <class... ARGS> tchecker::zg::zone_t * zone_allocate_and_construct(tche
*/
void zone_destruct_and_deallocate(tchecker::zg::zone_t * zone);
/*!
\brief factory of zones of a vcg
\param dim : the dimension
*/
std::shared_ptr<zone_t> factory(tchecker::clock_id_t dim);
/*!
\brief factory of zones of a vcg
\param zone : the zone to copy
*/
std::shared_ptr<zone_t> factory(zone_t const & zone);
} // end of namespace zg
/*!

18
src/CMakeLists.txt
View file

@ -46,17 +46,20 @@ add_subdirectory(algorithms)
add_subdirectory(clockbounds)
add_subdirectory(dbm)
add_subdirectory(expression)
add_subdirectory(extrapolation)
add_subdirectory(fsm)
add_subdirectory(graph)
add_subdirectory(parsing)
add_subdirectory(refzg)
add_subdirectory(statement)
add_subdirectory(strong-timed-bisim)
add_subdirectory(syncprod)
add_subdirectory(system)
add_subdirectory(ta)
add_subdirectory(ts)
add_subdirectory(utils)
add_subdirectory(variables)
add_subdirectory(vcg)
add_subdirectory(vm)
add_subdirectory(waiting)
add_subdirectory(zg)
@ -71,12 +74,14 @@ set(LIBTCHECKER_SRC
${CLOCKBOUNDS_SRC}
${DBM_SRC}
${EXPRESSION_SRC}
${EXTRAPOLATION_SRC}
${FSM_SRC}
${GRAPH_SRC}
${OTHER_SRC}
${PARSING_SRC}
${REFZG_SRC}
${STATEMENT_SRC}
${STRONG_TIMED_BISIM_SRC}
${SYNCPROD_SRC}
${SYSTEM_SRC}
${TA_SRC}
@ -84,6 +89,7 @@ set(LIBTCHECKER_SRC
${UTILS_SRC}
${VARIABLES_SRC}
${WAITING_SRC}
${VCG_SRC}
${VM_SRC}
${ZG_SRC})
@ -157,6 +163,16 @@ target_link_libraries(tck-simulate libtchecker_static ${Boost_LIBRARIES})
set_property(TARGET tck-simulate PROPERTY CXX_STANDARD 17)
set_property(TARGET tck-simulate PROPERTY CXX_STANDARD_REQUIRED ON)
# Build tck-compare executable
add_executable(tck-compare
${CMAKE_CURRENT_SOURCE_DIR}/tck-compare/tck-compare.cc
${CMAKE_CURRENT_SOURCE_DIR}/tck-compare/vcg-timed-bisim.hh
${CMAKE_CURRENT_SOURCE_DIR}/tck-compare/vcg-timed-bisim.cc)
target_link_libraries(tck-compare libtchecker_static ${Boost_LIBRARIES})
set_property(TARGET tck-compare PROPERTY CXX_STANDARD 17)
set_property(TARGET tck-compare PROPERTY CXX_STANDARD_REQUIRED ON)
# Project view in IDEs (Xcode, etc)
foreach(FILE ${LIBTCHECKER_SRC})
# Get the directory of the source file
@ -177,7 +193,7 @@ foreach(FILE ${LIBTCHECKER_SRC})
endforeach()
# Install rule for binaries, lib and header files
install(TARGETS tck-liveness tck-reach tck-simulate tck-syntax libtchecker_static
install(TARGETS tck-liveness tck-reach tck-simulate tck-syntax tck-compare libtchecker_static
RUNTIME DESTINATION bin
ARCHIVE DESTINATION lib)

50
src/dbm/dbm.cc
View file

@ -28,6 +28,18 @@ namespace dbm {
#define L(i) (i == 0 ? 0 : l[i - 1])
#define U(i) (i == 0 ? 0 : u[i - 1])
const tchecker::dbm::db_t * access(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t i, tchecker::clock_id_t j)
{
const tchecker::dbm::db_t * element = &(dbm[i*dim + j]);
return element;
}
tchecker::dbm::db_t * access(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t i, tchecker::clock_id_t j)
{
tchecker::dbm::db_t * element = &(dbm[i*dim + j]);
return element;
}
void copy(tchecker::dbm::db_t * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim)
{
std::memcpy(dbm1, dbm2, dim * dim * sizeof(*dbm2));
@ -341,7 +353,7 @@ void reset(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_
void reset(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_reset_container_t const & resets)
{
for (tchecker::clock_reset_t const & r : resets) {
tchecker::clock_id_t lid = (r.left_id() == tchecker::REFCLOCK_ID ? 0 : r.left_id() + 1);
tchecker::clock_id_t lid = (r.left_id() == tchecker::REFCLOCK_ID ? 0 : r.left_id() + 1); // It would be quite surprising if the lid would be reflock, right?
tchecker::clock_id_t rid = (r.right_id() == tchecker::REFCLOCK_ID ? 0 : r.right_id() + 1);
tchecker::dbm::reset(dbm, dim, lid, rid, r.value());
}
@ -512,6 +524,42 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d
return tchecker::dbm::tighten(dbm, dim);
}
tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone,
tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split,
tchecker::clock_reset_container_t reset)
{
// TODO: add assertions
if(reset.empty()) {
// place the dbm to return at the heap s.t. it is not destroyed during the returns
tchecker::dbm::db_t * result = (tchecker::dbm::db_t *)malloc(dim*dim*sizeof(tchecker::dbm::db_t));
tchecker::dbm::copy(result, zone_split, dim);
return result;
}
tchecker::dbm::db_t zone_clone[dim*dim];
tchecker::dbm::copy(zone_clone, orig_zone, dim);
tchecker::clock_reset_t cur = reset.back();
reset.pop_back();
if(cur.right_id() != tchecker::REFCLOCK_ID || cur.value() != 0) {
throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed");
}
tchecker::dbm::reset(zone_clone, dim, reset);
tchecker::dbm::free_clock(zone_split, dim, cur);
tchecker::dbm::db_t new_split[dim*dim];
intersection(new_split, zone_clone, zone_split, dim);
return revert_multiple_reset(orig_zone, dim, new_split, reset);
}
void extra_m(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::integer_t const * m)
{
assert(dbm != nullptr);

20
src/extrapolation/CMakeLists.txt Normal file
View file

@ -0,0 +1,20 @@
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
set(EXTRAPOLATION_SRC
${CMAKE_CURRENT_SOURCE_DIR}/extrapolation.cc
${CMAKE_CURRENT_SOURCE_DIR}/extrapolation_factory.cc
${CMAKE_CURRENT_SOURCE_DIR}/global_lu_extrapolation.cc
${CMAKE_CURRENT_SOURCE_DIR}/global_m_extrapolation.cc
${CMAKE_CURRENT_SOURCE_DIR}/k_norm.cc
${CMAKE_CURRENT_SOURCE_DIR}/local_lu_extrapolation.cc
${CMAKE_CURRENT_SOURCE_DIR}/local_m_extrapolation.cc
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/extrapolation.hh
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/extrapolation_factory.hh
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/global_lu_extrapolation.hh
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/global_m_extrapolation.hh
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/k_norm.hh
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/local_lu_extrapolation.hh
${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/local_m_extrapolation.hh
PARENT_SCOPE)

22
src/extrapolation/extrapolation.cc Normal file
View file

@ -0,0 +1,22 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/extrapolation/extrapolation.hh"
#include "tchecker/extrapolation/extrapolation_factory.hh"
#include "tchecker/clockbounds/solver.hh"
namespace tchecker {
namespace zg {
/* no_extrapolation_t */
void no_extrapolation_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) {}
} // end of namespace zg
} // end of namespace tchecker

147
src/extrapolation/extrapolation_factory.cc Normal file
View file

@ -0,0 +1,147 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include <memory>
#include "tchecker/extrapolation/extrapolation_factory.hh"
#include "tchecker/extrapolation/extrapolation.hh"
#include "tchecker/clockbounds/solver.hh"
#include "tchecker/basictypes.hh"
#include "tchecker/extrapolation/extrapolation.hh"
#include "tchecker/extrapolation/global_lu_extrapolation.hh"
#include "tchecker/extrapolation/global_m_extrapolation.hh"
#include "tchecker/extrapolation/k_norm.hh"
#include "tchecker/extrapolation/local_lu_extrapolation.hh"
#include "tchecker/extrapolation/local_m_extrapolation.hh"
namespace tchecker {
namespace zg {
/* factories */
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::ta::system_t const & system)
{
if (extrapolation_type == tchecker::zg::NO_EXTRAPOLATION)
return new tchecker::zg::no_extrapolation_t;
std::unique_ptr<tchecker::clockbounds::clockbounds_t> clock_bounds{tchecker::clockbounds::compute_clockbounds(system)};
if (clock_bounds.get() == nullptr)
return nullptr;
return tchecker::zg::extrapolation_factory(extrapolation_type, *clock_bounds);
}
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::clockbounds::clockbounds_t const & clock_bounds)
{
if (extrapolation_type == tchecker::zg::NO_EXTRAPOLATION)
return new tchecker::zg::no_extrapolation_t;
switch (extrapolation_type) {
case tchecker::zg::EXTRA_LU_GLOBAL:
return new tchecker::zg::global_extra_lu_t{clock_bounds.global_lu_map()};
case tchecker::zg::EXTRA_LU_LOCAL:
return new tchecker::zg::local_extra_lu_t{clock_bounds.local_lu_map()};
case tchecker::zg::EXTRA_LU_PLUS_GLOBAL:
return new tchecker::zg::global_extra_lu_plus_t{clock_bounds.global_lu_map()};
case tchecker::zg::EXTRA_LU_PLUS_LOCAL:
return new tchecker::zg::local_extra_lu_plus_t{clock_bounds.local_lu_map()};
case tchecker::zg::EXTRA_M_GLOBAL:
return new tchecker::zg::global_extra_m_t{clock_bounds.global_m_map()};
case tchecker::zg::EXTRA_M_LOCAL:
return new tchecker::zg::local_extra_m_t{clock_bounds.local_m_map()};
case tchecker::zg::EXTRA_M_PLUS_GLOBAL:
return new tchecker::zg::global_extra_m_plus_t{clock_bounds.global_m_map()};
case tchecker::zg::EXTRA_M_PLUS_LOCAL:
return new tchecker::zg::local_extra_m_plus_t{clock_bounds.local_m_map()};
case tchecker::zg::EXTRA_K_NORM:
return new tchecker::zg::k_norm{clock_bounds.global_lu_map()};
default:
throw std::invalid_argument("Unknown zone extrapolation");
}
}
} // end of namespace zg
namespace vcg {
tchecker::zg::extrapolation_t * extrapolation_factory(
enum tchecker::zg::extrapolation_type_t type,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_first,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_second,
bool first_not_second)
{
if(tchecker::zg::EXTRA_K_NORM != type)
throw std::invalid_argument("vcg currently supports k normalization only.");
std::vector<std::vector<tchecker::clockbounds::bound_t>> bounds;
bounds.push_back(std::vector<tchecker::clockbounds::bound_t>());
bounds.push_back(std::vector<tchecker::clockbounds::bound_t>());
for(std::size_t i = 0; i < 2; ++i) {
std::unique_ptr<tchecker::clockbounds::clockbounds_t> clock_bounds{
tchecker::clockbounds::compute_clockbounds(0 == i ? *orig_system_first : *orig_system_second)};
if (clock_bounds.get() == nullptr)
return nullptr;
std::shared_ptr<tchecker::clockbounds::global_lu_map_t> lu_map = clock_bounds->global_lu_map();
// we set the upper and lower clock bound to the same value to receive k-norm.
tchecker::clockbounds::map_t *U = const_cast<tchecker::clockbounds::map_t*>(&(lu_map->U()));
tchecker::clockbounds::map_t *L = const_cast<tchecker::clockbounds::map_t*>(& (lu_map->L()));
tchecker::clockbounds::update(*U, *L);
for(tchecker::clock_id_t j = 0; j < clock_bounds->clock_number(); ++j) {
bounds[i].push_back(U[0][j]);
}
}
tchecker::clock_id_t no_of_virtual_clocks = orig_system_first->clocks_count(VK_FLATTENED) + orig_system_second->clocks_count(VK_FLATTENED);
tchecker::clock_id_t no_of_original_clocks = first_not_second ? orig_system_first->clocks_count(VK_FLATTENED) : orig_system_second->clocks_count(VK_FLATTENED);
tchecker::clock_id_t no_of_clocks = no_of_original_clocks + no_of_virtual_clocks;
std::shared_ptr<tchecker::clockbounds::global_lu_map_t> resulting_clock_bounds = std::make_shared<tchecker::clockbounds::global_lu_map_t>(no_of_clocks);
/* set the bounds */
// original
for(tchecker::clock_id_t i = 0; i < no_of_original_clocks; ++i) {
tchecker::clockbounds::bound_t bound = first_not_second ? bounds[0][i] : bounds[1][i];
tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bound);
tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bound);
}
// first virtual
for(tchecker::clock_id_t i = no_of_original_clocks; i < no_of_original_clocks + orig_system_first->clocks_count(VK_FLATTENED); ++i) {
tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bounds[0][i - no_of_original_clocks]);
tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bounds[0][i - no_of_original_clocks]);
}
// second virtual
tchecker::clock_id_t offset_second_virtual = no_of_original_clocks + orig_system_first->clocks_count(VK_FLATTENED);
for(tchecker::clock_id_t i = offset_second_virtual; i < no_of_clocks; ++i) {
tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bounds[1][i - offset_second_virtual]);
tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bounds[1][i - offset_second_virtual]);
}
return new tchecker::vcg::k_norm_virtual{resulting_clock_bounds};
}
} // end of namespace vcg
} // end of namespace tchecker

43
src/extrapolation/global_lu_extrapolation.cc Normal file
View file

@ -0,0 +1,43 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/extrapolation/global_lu_extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
global_lu_extrapolation_t::global_lu_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds)
: _clock_bounds(clock_bounds)
{
}
} // end of namespace details
/* global_extra_lu_t */
void global_extra_lu_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_lu(dbm, dim, _clock_bounds->L().ptr(), _clock_bounds->U().ptr());
}
/* global_extra_lu_plus_t */
void global_extra_lu_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_lu_plus(dbm, dim, _clock_bounds->L().ptr(), _clock_bounds->U().ptr());
}
} // enf of namespace zg
} // end of namespace tchecker

43
src/extrapolation/global_m_extrapolation.cc Normal file
View file

@ -0,0 +1,43 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/extrapolation/global_m_extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
global_m_extrapolation_t::global_m_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::global_m_map_t const> const & clock_bounds)
: _clock_bounds(clock_bounds)
{
}
} // end of namespace details
/* global_extra_m_t */
void global_extra_m_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_m(dbm, dim, _clock_bounds->M().ptr());
}
/* global_extra_m_plus_t */
void global_extra_m_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_m_plus(dbm, dim, _clock_bounds->M().ptr());
}
} // end of namespace zg
} // end of namespace tchecker

39
src/extrapolation/k_norm.cc Normal file
View file

@ -0,0 +1,39 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/extrapolation/k_norm.hh"
namespace tchecker {
namespace zg {
k_norm::k_norm(
std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds)
:tchecker::zg::global_extra_lu_t(clock_bounds)
{
// k-norm is equivalent to global_extra_lu_t, if we always choose the maximum value of U(i) and L(i) for all checks.
tchecker::clockbounds::map_t *U = const_cast<tchecker::clockbounds::map_t*>(&(_clock_bounds->U()));
tchecker::clockbounds::map_t *L = const_cast<tchecker::clockbounds::map_t*>(& (_clock_bounds->L()));
tchecker::clockbounds::update(*U, *L);
tchecker::clockbounds::update(*L, *U);
}
} // end of namespace zg
namespace vcg {
k_norm_virtual::k_norm_virtual(
std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds)
:tchecker::zg::global_extra_lu_t(clock_bounds)
{
}
} // end of namespace vcg
} // end of namespace tchecker

93
src/extrapolation/local_lu_extrapolation.cc Normal file
View file

@ -0,0 +1,93 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/extrapolation/local_lu_extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
local_lu_extrapolation_t::local_lu_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::local_lu_map_t const> const & clock_bounds)
: _l(nullptr), _u(nullptr), _clock_bounds(clock_bounds)
{
_l = tchecker::clockbounds::allocate_map(_clock_bounds->clock_number());
_u = tchecker::clockbounds::allocate_map(_clock_bounds->clock_number());
}
local_lu_extrapolation_t::local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t const & e)
: _clock_bounds(e._clock_bounds)
{
_l = tchecker::clockbounds::clone_map(*e._l);
_u = tchecker::clockbounds::clone_map(*e._u);
}
local_lu_extrapolation_t::local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t && e)
: _l(std::move(e._l)), _u(std::move(e._u)), _clock_bounds(std::move(e._clock_bounds))
{
e._l = nullptr;
e._u = nullptr;
}
local_lu_extrapolation_t::~local_lu_extrapolation_t()
{
tchecker::clockbounds::deallocate_map(_l);
tchecker::clockbounds::deallocate_map(_u);
}
tchecker::zg::details::local_lu_extrapolation_t &
local_lu_extrapolation_t::operator=(tchecker::zg::details::local_lu_extrapolation_t const & e)
{
if (this != &e) {
_clock_bounds = e._clock_bounds;
tchecker::clockbounds::deallocate_map(_l);
_l = tchecker::clockbounds::clone_map(*e._l);
tchecker::clockbounds::deallocate_map(_u);
_u = tchecker::clockbounds::clone_map(*e._u);
}
return *this;
}
tchecker::zg::details::local_lu_extrapolation_t &
local_lu_extrapolation_t::operator=(tchecker::zg::details::local_lu_extrapolation_t && e)
{
if (this != &e) {
_clock_bounds = std::move(e._clock_bounds);
_l = std::move(e._l);
_u = std::move(e._u);
e._l = nullptr;
e._u = nullptr;
}
return *this;
}
} // end of namespace details
/* local_extra_lu_t */
void local_extra_lu_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_l, *_u);
tchecker::dbm::extra_lu(dbm, dim, _l->ptr(), _u->ptr());
}
/* local_extra_lu_plus_t */
void local_extra_lu_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_l, *_u);
tchecker::dbm::extra_lu_plus(dbm, dim, _l->ptr(), _u->ptr());
}
} // end of namespace zg
} // end of namespace tchecker

87
src/extrapolation/local_m_extrapolation.cc Normal file
View file

@ -0,0 +1,87 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_ZG_EXTRAPOLATION_LOCAL_M_EXTRAPOLATION_HH
#define TCHECKER_ZG_EXTRAPOLATION_LOCAL_M_EXTRAPOLATION_HH
#include "tchecker/extrapolation/local_m_extrapolation.hh"
#include "tchecker/extrapolation/extrapolation.hh"
namespace tchecker {
namespace zg {
namespace details {
local_m_extrapolation_t::local_m_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::local_m_map_t const> const & clock_bounds)
: _m(nullptr), _clock_bounds(clock_bounds)
{
_m = tchecker::clockbounds::allocate_map(_clock_bounds->clock_number());
}
local_m_extrapolation_t::local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t const & e)
: _m(nullptr), _clock_bounds(e._clock_bounds)
{
_m = tchecker::clockbounds::clone_map(*e._m);
}
local_m_extrapolation_t::local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t && e)
: _m(std::move(e._m)), _clock_bounds(std::move(e._clock_bounds))
{
e._m = nullptr;
}
local_m_extrapolation_t::~local_m_extrapolation_t() { tchecker::clockbounds::deallocate_map(_m); }
tchecker::zg::details::local_m_extrapolation_t &
local_m_extrapolation_t::operator=(tchecker::zg::details::local_m_extrapolation_t const & e)
{
if (this != &e) {
tchecker::clockbounds::deallocate_map(_m);
_m = tchecker::clockbounds::clone_map(*e._m);
_clock_bounds = e._clock_bounds;
}
return *this;
}
tchecker::zg::details::local_m_extrapolation_t &
local_m_extrapolation_t::operator=(tchecker::zg::details::local_m_extrapolation_t && e)
{
if (this != &e) {
_m = std::move(e._m);
e._m = nullptr;
_clock_bounds = std::move(e._clock_bounds);
}
return *this;
}
} // end of namespace details
/* local_extra_m_t */
void local_extra_m_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_m);
tchecker::dbm::extra_m(dbm, dim, _m->ptr());
}
/* local_extra_m_plus_t */
void local_extra_m_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_m);
tchecker::dbm::extra_m_plus(dbm, dim, _m->ptr());
}
} // enf of namespace zg
} // end of namespace tchecker
#endif

9
src/strong-timed-bisim/CMakeLists.txt Normal file
View file

@ -0,0 +1,9 @@
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
set(STRONG_TIMED_BISIM_SRC
${CMAKE_CURRENT_SOURCE_DIR}/stats.cc
${CMAKE_CURRENT_SOURCE_DIR}/virtual_clock_algorithm.cc
${CMAKE_CURRENT_SOURCE_DIR}/system.cc
PARENT_SCOPE)

49
src/strong-timed-bisim/stats.cc Normal file
View file

@ -0,0 +1,49 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include <sstream>
#include "tchecker/strong-timed-bisim/stats.hh"
namespace tchecker {
namespace strong_timed_bisim {
stats_t::stats_t() : _visited_pair_of_states(0), _visited_transitions(0), _deepest_path(0), _relationship_fulfilled(true) {}
unsigned long stats_t::visited_pair_of_states() const { return _visited_pair_of_states; }
unsigned long stats_t::visited_transitions() const { return _visited_transitions; }
unsigned long stats_t::deepest_path() const { return _deepest_path; }
bool stats_t::relationship_fulfilled() const { return _relationship_fulfilled; }
void stats_t::attributes(std::map<std::string, std::string> & m) const {
tchecker::algorithms::stats_t::attributes(m);
std::stringstream sstream;
sstream << _visited_pair_of_states;
m["VISITED_PAIR_OF_STATES_STATES"] = sstream.str();
sstream.str("");
sstream << _visited_transitions;
m["VISITED_TRANSITIONS"] = sstream.str();
sstream.str("");
sstream << _deepest_path;
m["DEEPEST_PATH"] = sstream.str();
sstream.str("");
sstream << std::boolalpha << _relationship_fulfilled;
m["RELATIONSHIP_FULFILLED"] = sstream.str();
}
} // end of namespace algorithms
} // end of namespace tchecker

36
src/strong-timed-bisim/system.cc Normal file
View file

@ -0,0 +1,36 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/strong-timed-bisim/system.hh"
#include <string>
namespace tchecker {
namespace strong_timed_bisim {
system_virtual_clocks_t::system_virtual_clocks_t(tchecker::ta::system_t const & system, std::size_t no_of_virtual_clocks, bool first_not_second)
: tchecker::ta::system_t(system),
_first_not_second(first_not_second),
_no_of_virtual_clocks(no_of_virtual_clocks) {
for(std::size_t i = 0; i < _no_of_virtual_clocks; ++i) {
std::shared_ptr<std::string const> virtual_clock_name = std::make_shared<std::string const>(VIRTUAL_CLOCK_PREFIX + to_string(i));
this->add_clock(*virtual_clock_name);
}
}
tchecker::clock_id_t system_virtual_clocks_t::get_no_of_virtual_clocks() const
{
return _no_of_virtual_clocks;
}
} // end of namespace strong_timed_bisim
} // end of namespace tchecker

110
src/strong-timed-bisim/virtual_clock_algorithm.cc Normal file
View file

@ -0,0 +1,110 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/strong-timed-bisim/virtual_clock_algorithm.hh"
#include "tchecker/vcg/virtual_constraint.hh"
namespace tchecker {
namespace strong_timed_bisim {
Lieb_et_al::Lieb_et_al(std::shared_ptr<tchecker::vcg::vcg_t> input_first, std::shared_ptr<tchecker::vcg::vcg_t> input_second) : _A(input_first), _B(input_first) {}
tchecker::strong_timed_bisim::stats_t Lieb_et_al::run() {
std::cout << "run algorithm" << std::endl;
stats_t stats;
#if 0
stats.set_start_time();
// sst is a tuple (tchecker::state_status_t, state_t, transition_t)
// state_status_t : see basictypes.hh
std::vector<tchecker::zg::zg_t::sst_t> sst_first;
std::vector<tchecker::zg::zg_t::sst_t> sst_second;
this->_A->initial(sst_first);
this->_B->initial(sst_second);
if(STATE_OK != std::get<0>(sst_first[0]) || STATE_OK != std::get<0>(sst_second[0]))
throw std::runtime_error("problems with initial state");
std::size_t dim = std::get<1>(sst_first[0])->zone().dim();
auto dbm = std::get<1>(sst_first[0])->zone().dbm();
for(std::size_t i = 0; i < dim; ++i) {
for(std::size_t j = 0; j < dim; ++j) {
std::size_t index = i*dim + j;
std::cout << "(" << dbm[index].cmp << ", " << dbm[index].value << ") ";
}
std::cout << std::endl;
}
tchecker::virtual_constraint::virtual_constraint_t *vc = tchecker::virtual_constraint::factory(&(std::get<1>(sst_first[0])->zone()), this->_A->get_no_of_virtual_clocks());
const clock_constraint_container_t & virt_cons = vc->get_vc(this->_A->clocks_count() - this->_A->get_no_of_virtual_clocks());
for(auto iter = virt_cons.begin(); iter < virt_cons.end(); iter++) {
std::cout << *iter << std::endl;
}
/*
for(std::size_t i = 0; i <= input_first->get_no_of_virtual_clocks(); ++i) {
for(std::size_t j = 0; j < input_first->get_no_of_virtual_clocks(); ++j) {
std::size_t index = i*input_first->get_no_of_virtual_clocks() + i + j;
std::cout << "(" << (vc->get_dbm())[index].cmp << ", " << (vc->get_dbm())[index].value << ") ";
}
std::cout << std::endl;
}
*/
delete vc;
stats.set_end_time();
#endif
return stats;
}
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t symb_state_first,
std::shared_ptr<tchecker::vcg::vcg_t> vcg_first,
tchecker::zg::const_state_sptr_t symb_state_second,
std::shared_ptr<tchecker::vcg::vcg_t> vcg_second,
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
(*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t))
{
std::vector<tchecker::vcg::vcg_t::sst_t> v_first;
vcg_first->next(symb_state_first, v_first);
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> result
= std::make_shared<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(vcg_first->get_no_of_virtual_clocks());
for (auto && [status_first, s_first, t_first] : v_first) {
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> lo_result;
std::vector<tchecker::vcg::vcg_t::sst_t> v_second;
vcg_second->next(symb_state_second, v_second);
for (auto && [status_second, s_second, t_second] : v_first) {
if(t_first->vedge().event_equal(vcg_first->system(), t_second->vedge(), vcg_second->system())) {
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> inter = func(s_first, s_second);
for(auto iter = inter->begin(); iter < inter->end(); iter++) {
// TODO
}
}
}
}
}
} // end of namespace strong_timed_bisim
} // end ofnamespace tchecker

25
src/syncprod/vedge.cc
View file

@ -6,6 +6,7 @@
*/
#include <sstream>
#include <set>
#include "tchecker/syncprod/vedge.hh"
#include "tchecker/utils/ordering.hh"
@ -46,6 +47,30 @@ tchecker::vedge_t::const_array_iterator_t vedge_t::begin_array() const { return
tchecker::vedge_t::const_array_iterator_t vedge_t::end_array() const { return tchecker::edge_array_t::end(); }
bool vedge_t::contains_events(const tchecker::system::system_t & my_system, const vedge_t & other, const tchecker::system::system_t & other_system) const
{
std::set<std::string> to_check;
for(auto it = other.begin(); it != other.end(); it++) {
std::string cur = other_system.event_name(other_system.edge(*it)->event_id());
to_check.insert(cur);
}
std::set<std::string> contained;
for(auto it = this->begin(); it != this->end(); it++) {
std::string cur = my_system.event_name(my_system.edge(*it)->event_id());
contained.insert(cur);
}
for(auto it = to_check.begin(); it != to_check.end(); it++) {
if(contained.end() == contained.find(*it)) {
return false;
}
}
return true;
}
void vedge_destruct_and_deallocate(tchecker::vedge_t * vedge)
{
tchecker::vedge_t::destruct(vedge);

229
src/tck-compare/tck-compare.cc Normal file
View file

@ -0,0 +1,229 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include <fstream>
#include <getopt.h>
#include <iostream>
#include <limits>
#include <map>
#include <memory>
#include <string>
#include <string.h>
#include "vcg-timed-bisim.hh"
/*
\file tck-compare.cc
\brief Comparison of timed automata
*/
static struct option long_options[] = {{"relationship", required_argument, 0, 'r'},
{"order", required_argument, 0, 'n'},
{"output", required_argument, 0, 'o'},
{"help", no_argument, 0, 'h'},
{"block-size", required_argument, 0, 0},
{"table-size", required_argument, 0, 0},
{0, 0, 0, 0}};
static char const * const options = (char *)"hr:n:";
/*!
\brief Display usage
\param progname : programme name
*/
void usage(char * progname)
{
std::cerr << "Usage: " << progname << " [options] [file1] [file2]" << std::endl;
std::cerr << " -r relationship relationship to check" << std::endl;
std::cerr << " strong-timed-bisim strong timed bisimilarity" << std::endl;
std::cerr << " -n order the order in which the relationship shall be checked" << std::endl
<< std::endl;
std::cerr << " -h help" << std::endl;
std::cerr << " -o out_file output file for certificate (default is standard output)" << std::endl;
}
enum relationship_t {
STRONG_TIMED_BISIM, /*!< Strong Timed Bisimilarity */
};
enum relationship_t relationship = STRONG_TIMED_BISIM; /*!< Selected relationship */
unsigned int order = std::numeric_limits<unsigned int>::max();
bool help = false; /*!< Help flag */
std::string output_file = ""; /*!< Output file name (empty means standard output) */
std::ostream * os = &std::cout; /*!< Default output stream */
std::size_t block_size = 10000; /*!< Size of allocated blocks */
std::size_t table_size = 65536; /*!< Size of hash tables */
/*!
\brief Parse command-line arguments
\param argc : number of arguments
\param argv : array of arguments
\pre argv[0] up to argv[argc-1] are valid accesses
\post global variables help, output_file, search_order and labels have been set
from argv
*/
int parse_command_line(int argc, char * argv[])
{
while (true) {
int long_option_index = -1;
int c = getopt_long(argc, argv, options, long_options, &long_option_index);
if (c == -1)
break;
if (c == ':')
throw std::runtime_error("Missing option parameter");
else if (c == '?')
throw std::runtime_error("Unknown command-line option");
else if (c != 0) {
switch (c) {
case 'r':
if (strcmp(optarg, "strong-timed-bisim") == 0)
relationship = STRONG_TIMED_BISIM;
else
throw std::runtime_error("Unknow relationship: " + std::string(optarg));
break;
case 'n':
order = std::stoul(optarg);
break;
case 'o':
output_file = optarg;
break;
case 'h':
help = true;
break;
default:
throw std::runtime_error("This should never be executed");
break;
}
}
else {
if (strcmp(long_options[long_option_index].name, "block-size") == 0)
block_size = std::strtoull(optarg, nullptr, 10);
else if (strcmp(long_options[long_option_index].name, "table-size") == 0)
table_size = std::strtoull(optarg, nullptr, 10);
else
throw std::runtime_error("This also should never be executed");
}
}
return optind;
}
/*!
\brief Load a system declaration from a file
\param filename : file name
\return pointer to a system declaration loaded from filename, nullptr in case
of errors
\post all errors have been reported to std::cerr
*/
tchecker::parsing::system_declaration_t * load_system_declaration(std::string const & filename)
{
tchecker::parsing::system_declaration_t * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(filename);
if (sysdecl == nullptr)
throw std::runtime_error("nullptr system declaration");
}
catch (std::exception const & e) {
std::cerr << tchecker::log_error << e.what() << std::endl;
}
return sysdecl;
}
/*!
\brief Perform strong timed bisimilarity check
\param sysdecl_first : system declaration of the first TA
\param sysdecl_first : system declaration of the second TA
\post statistics on strong timed bisimilarity analysis of the system declared by sysdecl have been output to standard output.
*/
void strong_timed_bisim(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_first, std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_second)
{
std::cout << "tck-compare.cc: run" << std::endl;
auto stats = tchecker::tck_compare::vcg_timed_bisim::run(sysdecl_first, sysdecl_second, os, block_size, table_size);
std::cerr << "tck-compare.cc : print stats" << std::endl;
// stats
std::map<std::string, std::string> m;
stats.attributes(m);
for (auto && [key, value] : m)
std::cout << key << " " << value << std::endl;
}
/*
\brief Main function
*/
int main(int argc, char * argv[]) {
try{
int optindex = parse_command_line(argc, argv);
if (argc - optindex != 2) {
std::cerr << "exactly two input files needed" << std::endl;
usage(argv[0]);
return EXIT_FAILURE;
}
if (help) {
usage(argv[0]);
return EXIT_SUCCESS;
}
std::string first_input = argv[argc - 2];
std::shared_ptr<tchecker::parsing::system_declaration_t> sysdecl_first_TA{load_system_declaration(first_input)};
std::string second_input = argv[argc - 1];
std::shared_ptr<tchecker::parsing::system_declaration_t> sysdecl_second_TA{load_system_declaration(second_input)};
if (tchecker::log_error_count() > 0)
return EXIT_FAILURE;
std::shared_ptr<std::ofstream> os_ptr{nullptr};
if (output_file != "") {
try {
os_ptr = std::make_shared<std::ofstream>(output_file);
os = os_ptr.get();
}
catch (std::exception & e) {
std::cerr << tchecker::log_error << e.what() << std::endl;
return EXIT_FAILURE;
}
}
if(STRONG_TIMED_BISIM == relationship) {
strong_timed_bisim(sysdecl_first_TA, sysdecl_second_TA);
} else {
throw std::runtime_error("Unknown relationship");
}
}
catch (std::exception & e) {
std::cerr << tchecker::log_error << e.what() << std::endl;
return EXIT_FAILURE;
}
return EXIT_SUCCESS;
}

192
src/tck-compare/vcg-timed-bisim.cc Normal file
View file

@ -0,0 +1,192 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "vcg-timed-bisim.hh"
#include <string>
#include <memory>
#include "tchecker/system/static_analysis.hh"
#include "tchecker/ta/system.hh"
#include "tchecker/strong-timed-bisim/virtual_clock_algorithm.hh"
#include "tchecker/strong-timed-bisim/system.hh"
#include "tchecker/zg/zg.hh"
#define FIRST_PRODUCT_NAME "A"
#define SECOND_PRODUCT_NAME "B"
#define LOC_DELIMITER "__"
/* run */
namespace tchecker {
namespace tck_compare {
namespace vcg_timed_bisim {
void check_for_init(std::shared_ptr<tchecker::system::system_t> const system){
auto init_loc = system->initial_locations(0);
auto iter = init_loc.begin();
if (iter == init_loc.end()) {
std::string error_message{"Currently, strong timed bisim is supported with exactly a single initial location per process, only\na process of "};
error_message.append(system->name());
error_message.append(" has no initial location");
throw std::runtime_error(error_message);
}
++iter;
if (iter != init_loc.end()) {
std::string error_message{"Currently, strong timed bisim is supported with exactly a single initial location per process, only\na process of "};
error_message.append(system->name());
error_message.append(" has more than a single initial location");
throw std::runtime_error(error_message);
}
}
tchecker::clock_id_t clocks_check(std::shared_ptr<tchecker::ta::system_t> const system) {
std::size_t result = 0;
auto p_c = system->clock_variables().identifiers();
auto begin_p_c = p_c.begin(), end_p_c = p_c.end();
for(auto it = begin_p_c; it != end_p_c; ++it) {
std::string clock_name{system->clock_name(it)};
if (clock_name.rfind(VIRTUAL_CLOCK_PREFIX, 0) == 0) {
std::string error_message{"The clock prefix "};
error_message.append(VIRTUAL_CLOCK_PREFIX);
error_message.append(" is reserved for virtual clocks and should not be used by the TA.");
throw std::runtime_error(error_message);
}
++result;
}
return system->clocks_count(VK_FLATTENED);
}
tchecker::strong_timed_bisim::stats_t
run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_first, std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_second,
std::ostream * os, std::size_t block_size, std::size_t table_size) {
std::vector<std::shared_ptr<tchecker::ta::system_t>> systems;
std::cout << "vcg-timed-bisim.cc : run" << std::endl;
for(size_t i = 0; i < 2; ++i) {
std::shared_ptr<tchecker::ta::system_t> cur_system{new tchecker::ta::system_t{ (i == 0) ? *sysdecl_first : *sysdecl_second}};
std::shared_ptr<tchecker::syncprod::system_t const> system_syncprod = std::make_shared<tchecker::syncprod::system_t const>(cur_system->as_syncprod_system());
std::shared_ptr<tchecker::system::system_t> product = std::make_shared<tchecker::system::system_t>(tchecker::syncprod::synchronized_product(system_syncprod, (i == 0) ? FIRST_PRODUCT_NAME : SECOND_PRODUCT_NAME, LOC_DELIMITER));
check_for_init(product);
systems.push_back(cur_system);
}
tchecker::clock_id_t no_of_virt_clocks = clocks_check(systems[0]) + clocks_check(systems[1]);
std::vector<std::shared_ptr<tchecker::vcg::vcg_t>> vcgs;
for(size_t i = 0; i < 2; ++i) {
std::shared_ptr<tchecker::strong_timed_bisim::system_virtual_clocks_t const> extended_system{new tchecker::strong_timed_bisim::system_virtual_clocks_t{*(systems[i]), no_of_virt_clocks, 0 == i}};
std::shared_ptr<tchecker::vcg::vcg_t> vcg{tchecker::vcg::factory(extended_system, 0 == i, systems[0], systems[1], tchecker::ts::SHARING, tchecker::zg::DISTINGUISHED_SEMANTICS,
tchecker::zg::EXTRA_K_NORM, block_size, table_size)};
vcgs.push_back(vcg);
}
std::cout << "vcg-timed-bisim.cc : created vcgs" << std::endl;
auto algorithm = new tchecker::strong_timed_bisim::Lieb_et_al(vcgs[0], vcgs[1]);
return algorithm->run();
/* DELETE ME!
std::cout << "no. of processes: " << system_first->processes_count() << std::endl;
std::cout << "no. of processes of product: " << product_first->processes_count() << std::endl;
auto r = system_first->attributes().range();
auto begin = r.begin(), end = r.end();
std::cout << "loop system attributes" << std::endl;
for(auto it = begin; it != end; ++it) {
std::cout << "found attribute: " << (*it).key() << ":" << (*it).value() << std::endl;
}
auto p = product_first->attributes().range();
auto pbegin = p.begin(), pend = p.end();
std::cout << "loop product attributes" << std::endl;
for(auto it = pbegin; it != pend; ++it) {
std::cout << "found attribute: " << (*it).key() << ":" << (*it).value() << std::endl;
}
auto r_l = system_first->locations();
auto begin_l = r_l.begin(), end_l = r_l.end();
std::cout << "loop system locations" << std::endl;
for(auto it = begin_l; it != end_l; ++it) {
std::cout << "found location: " << (*it)->name() << std::endl;
}
auto p_l = product_first->locations();
auto begin_p_l = p_l.begin(), end_p_l = p_l.end();
std::cout << "loop product locations" << std::endl;
for(auto it = begin_p_l; it != end_p_l; ++it) {
std::cout << "found location: " << (*it)->name() << std::endl;
}
std::cout << "initial system locations" << std::endl;
for(std::size_t i = 0; i < system_first->processes_count(); ++i) {
auto r_init = system_first->initial_locations(i);
auto begin_init = r_init.begin(), end_init = r_init.end();
for(auto it = begin_init; it != end_init; ++it) {
std::cout << "found initial location for process " << i << "(" << system_first->process_name(i) << "): " << (*it)->name() << std::endl;
}
}
std::cout << "initial product locations" << std::endl;
auto p_init = product_first->initial_locations(0);
auto begin_init = p_init.begin(), end_init = p_init.end();
for(auto it = begin_init; it != end_init; ++it) {
std::cout << "found initial location for process " << 0 << "(" << product_first->process_name(0) << "): " << (*it)->name() << std::endl;
}
auto r_c = system_first->clock_variables().identifiers();
auto begin_c = r_c.begin(), end_c = r_c.end();
std::cout << "loop system clocks" << std::endl;
for(auto it = begin_c; it != end_c; ++it) {
std::cout << "found clock: " << it << ": " << system_first->clock_name(it) << std::endl;
}
auto p_c = product_first->clock_variables().identifiers();
auto begin_p_c = p_c.begin(), end_p_c = p_c.end();
std::cout << "loop product clocks" << std::endl;
for(auto it = begin_p_c; it != end_p_c; ++it) {
std::cout << "found clock: " << it << ": " << product_first->clock_name(it) << std::endl;
}
/* UNTIL ME! */
}
} // end of namespace vcg_timed_bisim
} // end of namespace tck_compare
} // end of namespace tchecker

42
src/tck-compare/vcg-timed-bisim.hh Normal file
View file

@ -0,0 +1,42 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#ifndef TCHECKER_TCK_COMPARE_VCG_TIMED_BISIM_HH
#define TCHECKER_TCK_COMPARE_VCG_TIMED_BISIM_HH
#include <memory>
#include "tchecker/parsing/parsing.hh"
#include "tchecker/strong-timed-bisim/stats.hh"
namespace tchecker {
namespace tck_compare {
namespace vcg_timed_bisim {
/*!
\brief Run check for timed bisimilarity
\param sysdecl_first : first system declaration
\param sysdecl_first : first system declaration
\param block_size : number of elements allocated in one block
\param table_size : size of hash tables
\post
\return statistics on the run and the reachability graph
*/
tchecker::strong_timed_bisim::stats_t
run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_first, std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_second,
std::ostream * os, std::size_t block_size, std::size_t table_size);
} // end of namespace vcg_timed_bisim
} // end of namespace tck_compare
} // end of namespace tchecker
#endif // TCHECKER_TCK-COMPARE_VCG_TIMED_BISIM_HH

2
src/tck-liveness/zg-couvscc.cc
View file

@ -179,4 +179,4 @@ run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl, st
} // namespace tck_liveness
} // end of namespace tchecker
} // end of namespace tchecker

2
src/tck-liveness/zg-ndfs.cc
View file

@ -172,4 +172,4 @@ run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl, st
} // namespace tck_liveness
} // end of namespace tchecker
} // end of namespace tchecker

2
src/tck-reach/zg-covreach.cc
View file

@ -202,4 +202,4 @@ run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl, st
} // end of namespace tck_reach
} // end of namespace tchecker
} // end of namespace tchecker

2
src/tck-reach/zg-reach.cc
View file

@ -193,4 +193,4 @@ run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl, st
} // end of namespace tck_reach
} // end of namespace tchecker
} // end of namespace tchecker

2
src/tck-simulate/simulate.cc
View file

@ -237,4 +237,4 @@ void onestep_simulation(tchecker::parsing::system_declaration_t const & sysdecl,
} // namespace tck_simulate
} // namespace tchecker
} // namespace tchecker

2
src/utils/CMakeLists.txt
View file

@ -8,6 +8,7 @@ set(UTILS_SRC
${CMAKE_CURRENT_SOURCE_DIR}/iterator.cc
${CMAKE_CURRENT_SOURCE_DIR}/log.cc
${CMAKE_CURRENT_SOURCE_DIR}/string.cc
${CMAKE_CURRENT_SOURCE_DIR}/zone_container.cc
${TCHECKER_INCLUDE_DIR}/tchecker/utils/allocation_size.hh
${TCHECKER_INCLUDE_DIR}/tchecker/utils/array.hh
${TCHECKER_INCLUDE_DIR}/tchecker/utils/bitset.hh
@ -22,4 +23,5 @@ set(UTILS_SRC
${TCHECKER_INCLUDE_DIR}/tchecker/utils/singleton_pool.hh
${TCHECKER_INCLUDE_DIR}/tchecker/utils/spinlock.hh
${TCHECKER_INCLUDE_DIR}/tchecker/utils/string.hh
${TCHECKER_INCLUDE_DIR}/tchecker/utils/zone_container.hh
PARENT_SCOPE)

71
src/utils/zone_container.cc Normal file
View file

@ -0,0 +1,71 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/utils/zone_container.hh"
namespace tchecker {
zone_container_t<tchecker::zg::zone_t> contained_in_all(std::vector<zone_container_t<tchecker::zg::zone_t>> & zones, tchecker::clock_id_t dim)
{
if (zones.empty()) {
zone_container_t<tchecker::zg::zone_t> result(dim);
return result;
}
if (1 == zones.size()) {
return zones[0];
}
zone_container_t<tchecker::zg::zone_t> cur = zones.back();
zones.pop_back();
zone_container_t<tchecker::zg::zone_t> inter = contained_in_all(zones, dim);
zone_container_t<tchecker::zg::zone_t> result{dim};
for(auto iter_cur = cur.begin(); iter_cur < cur.end(); iter_cur++) {
for(auto iter_inter = inter.begin(); iter_inter < inter.end(); iter_inter++) {
std::shared_ptr<tchecker::zg::zone_t> tmp = tchecker::zg::factory(dim);
if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(tmp->dbm(), (**iter_cur).dbm(), (**iter_inter).dbm(), (**iter_cur).dim())) {
result.append_zone(tmp);
}
else {
tchecker::zg::zone_t::destruct(&(*tmp));
}
}
}
return result;
}
// specializations
template<>
std::shared_ptr<tchecker::zg::zone_t> zone_container_t<tchecker::zg::zone_t>::create_element()
{
return tchecker::zg::factory(_dim);
}
template<>
std::shared_ptr<tchecker::zg::zone_t> zone_container_t<tchecker::zg::zone_t>::create_element(tchecker::zg::zone_t const & zone)
{
return tchecker::zg::factory(zone);
}
template<>
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>::create_element()
{
return tchecker::virtual_constraint::factory(_dim);
}
template<>
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>::create_element(tchecker::virtual_constraint::virtual_constraint_t const & zone)
{
return tchecker::virtual_constraint::factory(zone);
}
} // end of namespace tchecker

14
src/vcg/CMakeLists.txt Normal file
View file

@ -0,0 +1,14 @@
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
set(VCG_SRC
${CMAKE_CURRENT_SOURCE_DIR}/revert_transitions.cc
${CMAKE_CURRENT_SOURCE_DIR}/sync.cc
${CMAKE_CURRENT_SOURCE_DIR}/vcg.cc
${CMAKE_CURRENT_SOURCE_DIR}/virtual_constraint.cc
${TCHECKER_INCLUDE_DIR}/tchecker/vcg/revert_transitions.hh
${TCHECKER_INCLUDE_DIR}/tchecker/vcg/sync.hh
${TCHECKER_INCLUDE_DIR}/tchecker/vcg/vcg.hh
${TCHECKER_INCLUDE_DIR}/tchecker/vcg/virtual_constraint.hh
PARENT_SCOPE)

73
src/vcg/revert_transitions.cc Normal file
View file

@ -0,0 +1,73 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/vcg/revert_transitions.hh"
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
revert_action_trans(const tchecker::zg::zone_t & zone,
const tchecker::clock_constraint_container_t & guard,
const tchecker::clock_reset_container_t & reset,
const tchecker::clock_constraint_container_t & tgt_invariant,
const tchecker::virtual_constraint::virtual_constraint_t & phi_split)
{
tchecker::clock_reset_container_t reset_copy;
reset_copy.reserve(reset.size());
std::copy(reset.begin(), reset.end(), reset_copy.begin());
tchecker::dbm::db_t zone_clone[zone.dim()*zone.dim()];
zone.to_dbm(zone_clone);
tchecker::dbm::db_t d_land_g[zone.dim()*zone.dim()];
zone.to_dbm(d_land_g);
tchecker::dbm::constrain(d_land_g, zone.dim(), guard);
tchecker::dbm::db_t r_d_land_g_land_phi[zone.dim()*zone.dim()];
tchecker::dbm::copy(r_d_land_g_land_phi, d_land_g, zone.dim());
tchecker::dbm::reset(r_d_land_g_land_phi, zone.dim(), reset);
tchecker::dbm::constrain(r_d_land_g_land_phi, zone.dim(), phi_split.get_vc(zone.dim() - phi_split.dim()));
tchecker::dbm::db_t *reverted = tchecker::dbm::revert_multiple_reset(d_land_g, zone.dim(), r_d_land_g_land_phi, reset_copy);
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> virt_mult_reset
= tchecker::virtual_constraint::factory(reverted, zone.dim(), phi_split.get_no_of_virt_clocks());
tchecker::dbm::constrain(zone_clone, zone.dim(), virt_mult_reset->get_vc(zone.dim() - phi_split.dim()));
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result
= tchecker::virtual_constraint::factory(zone_clone, zone.dim(), phi_split.get_no_of_virt_clocks());
return result;
}
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split)
{
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_copy = factory(phi_split);
tchecker::dbm::open_down(phi_copy->dbm(), phi_copy->dim());
std::shared_ptr<tchecker::zg::zone_t> zone_copy = tchecker::zg::factory(zone);
tchecker::dbm::constrain(zone_copy->dbm(), zone_copy->dim(), phi_copy->get_vc(zone_copy->dim() - phi_copy->dim()));
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result
= tchecker::virtual_constraint::factory(zone_copy, phi_split.get_no_of_virt_clocks());
tchecker::zg::zone_destruct_and_deallocate(&(*phi_copy));
tchecker::zg::zone_destruct_and_deallocate(&(*phi_copy));
return result;
}

101
src/vcg/sync.cc Normal file
View file

@ -0,0 +1,101 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/vcg/sync.hh"
#include "tchecker/dbm/dbm.hh"
void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim,
tchecker::clock_id_t lowest_virt_clk_id, tchecker::clock_id_t no_of_orig_clocks_1,
tchecker::clock_reset_container_t const & orig_reset1,
tchecker::clock_reset_container_t const & orig_reset2)
{
// TODO: add assertions
tchecker::clock_reset_container_t virt_resets;
for(const tchecker::clock_reset_t & r : orig_reset1) {
if(r.right_id() != tchecker::REFCLOCK_ID || r.value() != 0) {
throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed");
}
reset_to_value(dbm1, dim, r.left_id() + 1 + lowest_virt_clk_id, 0);
reset_to_value(dbm2, dim, r.left_id() + 1 + lowest_virt_clk_id, 0);
}
tchecker::clock_id_t border = lowest_virt_clk_id + no_of_orig_clocks_1;
for(const tchecker::clock_reset_t & r : orig_reset2) {
if(r.right_id() != tchecker::REFCLOCK_ID || r.value() != 0) {
throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed");
}
reset_to_value(dbm1, dim, r.left_id() + 1 + border, 0);
reset_to_value(dbm2, dim, r.left_id() + 1 + border, 0);
}
virt_resets.clear();
}
std::tuple<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>>
revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim,
const tchecker::virtual_constraint::virtual_constraint_t & phi_e, tchecker::clock_id_t lowest_virt_clk_id,
tchecker::clock_id_t no_of_orig_clocks_1)
{
// TODO add assertions
tchecker::dbm::db_t zero_value = tchecker::dbm::db(tchecker::LT, 0);
tchecker::clock_reset_container_t reset_set;
for(tchecker::clock_id_t i = 1; i < (dim - lowest_virt_clk_id); ++i) {
if(zero_value == *tchecker::dbm::access(dbm1, dim, i, 0) && zero_value == *tchecker::dbm::access(dbm1, dim, 0, i)) {
tchecker::clock_reset_t tmp{i + lowest_virt_clk_id - 1, tchecker::REFCLOCK_ID, 0};
reset_set.emplace_back(tmp);
}
}
for(tchecker::clock_id_t i = 1; i < (dim - lowest_virt_clk_id); ++i) {
if(zero_value == *tchecker::dbm::access(dbm2, dim, i, 0) && zero_value == *tchecker::dbm::access(dbm2, dim, 0, i)) {
tchecker::clock_reset_t tmp{i + lowest_virt_clk_id + no_of_orig_clocks_1 - 1, tchecker::REFCLOCK_ID, 0};
reset_set.emplace_back(tmp);
}
}
tchecker::dbm::db_t dbm1_clone[dim*dim];
tchecker::dbm::copy(dbm1_clone, dbm1, dim);
tchecker::dbm::constrain(dbm1_clone, dim, phi_e.get_vc(lowest_virt_clk_id - 1));
tchecker::dbm::db_t dbm2_clone[dim*dim];
tchecker::dbm::copy(dbm2_clone, dbm2, dim);
tchecker::dbm::constrain(dbm2_clone, dim, phi_e.get_vc(lowest_virt_clk_id - 1));
tchecker::dbm::db_t * multiple_reset = revert_multiple_reset(dbm1, dim, dbm1_clone, reset_set);
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> first
= tchecker::virtual_constraint::factory(multiple_reset, dim, dim - lowest_virt_clk_id);
free(multiple_reset);
multiple_reset = revert_multiple_reset(dbm2, dim, dbm2_clone, reset_set);
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> second
= tchecker::virtual_constraint::factory(multiple_reset, dim, dim - lowest_virt_clk_id);
free(multiple_reset);
reset_set.clear();
return std::make_tuple(first, second);
}

52
src/vcg/vcg.cc Normal file
View file

@ -0,0 +1,52 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/vcg/vcg.hh"
namespace tchecker {
namespace vcg {
vcg_t::vcg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
std::shared_ptr<tchecker::zg::semantics_t> const & semantics, tchecker::clock_id_t no_of_virtual_clocks,
std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size)
: tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size),
_no_of_virtual_clocks(no_of_virtual_clocks)
{
}
tchecker::clock_id_t vcg_t::get_no_of_virtual_clocks() const
{
return _no_of_virtual_clocks;
}
tchecker::vcg::vcg_t * factory(std::shared_ptr<tchecker::strong_timed_bisim::system_virtual_clocks_t const> const & extended_system,
bool first_not_second,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_first,
std::shared_ptr<tchecker::ta::system_t const> const & orig_system_second,
enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size,
std::size_t table_size)
{
std::shared_ptr<tchecker::zg::extrapolation_t> extrapolation{
tchecker::vcg::extrapolation_factory(extrapolation_type, orig_system_first, orig_system_second, first_not_second)};
if (extrapolation.get() == nullptr)
return nullptr;
std::shared_ptr<tchecker::zg::semantics_t> semantics{tchecker::zg::semantics_factory(semantics_type)};
tchecker::clock_id_t vc = extended_system->get_no_of_virtual_clocks();
return new tchecker::vcg::vcg_t(extended_system, sharing_type, semantics, vc, extrapolation, block_size, table_size);
}
} // end of namespace vcg
} // end of namespace tchecker

222
src/vcg/virtual_constraint.cc Normal file
View file

@ -0,0 +1,222 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/vcg/virtual_constraint.hh"
namespace tchecker {
namespace virtual_constraint {
const tchecker::clock_id_t virtual_constraint_t::get_no_of_virt_clocks() const
{
return this->dim() - 1;
}
// WARNING: above might not be tight after this call
void insert_values(std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> to_change, tchecker::clock_id_t i, tchecker::clock_id_t j)
{
tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(to_change->dbm(), to_change->dim(), j, i);
tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(to_change->dbm(), to_change->dim(), i, j);
tchecker::dbm::db_t db_above{
(tchecker::LE == tchecker::dbm::comparator(*i_minus_j)) ? tchecker::LT : tchecker::LE,
tchecker::dbm::value(*i_minus_j)};
*j_minus_i = db_above;
*i_minus_j = tchecker::dbm::LT_INFINITY;
}
// WARNING: The vitrual constraints placed at result are NOT tight!
void add_neg(tchecker::zone_container_t<virtual_constraint_t> *result, const virtual_constraint_t *cur, tchecker::clock_id_t i, tchecker::clock_id_t j)
{
// we first insert all clock valuations for which chi_i - chi_j is to high
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> above = tchecker::virtual_constraint::factory(*cur);
insert_values(above, i, j);
result->append_zone(above);
// now we insert all clocks for which chi_i - chi_j is to low
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> below = tchecker::virtual_constraint::factory(*cur);
insert_values(below, j, i);
result->append_zone(below);
}
tchecker::zone_container_t<virtual_constraint_t> * virtual_constraint_t::neg() const
{
tchecker::zone_container_t<virtual_constraint_t> inter{this->dim()};
for(tchecker::clock_id_t i = 0; i < this->dim(); ++i) {
for(tchecker::clock_id_t j = i+1; j < this->dim(); ++j) {
tchecker::clock_id_t size_before = inter.size();
add_neg(&inter, this, i, j);
// do the same for all already added virtual constraints.
for(tchecker::clock_id_t iter = 0; iter < size_before; ++iter) {
add_neg(&inter, &(*(inter[iter])), i, j);
}
}
}
tchecker::zone_container_t<virtual_constraint_t> * result = new tchecker::zone_container_t<virtual_constraint_t>(this->dim());
for(auto iter = inter.begin(); iter < inter.end(); iter++) {
if(tchecker::dbm::NON_EMPTY == tchecker::dbm::tighten((*iter)->dbm(), (*iter)->dim())) {
result->append_zone(*iter);
} else {
tchecker::virtual_constraint::destruct(&(**iter));
}
}
return result;
}
clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t orig_clocks_offset) const
{
clock_constraint_container_t result;
for(tchecker::clock_id_t i = 1; i < get_no_of_virt_clocks(); ++i) {
tchecker::clock_id_t cur = i + orig_clocks_offset;
result.emplace_back(0, cur, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->value);
result.emplace_back(cur, 0, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->value);
for(tchecker::clock_id_t j = i+1; j < get_no_of_virt_clocks(); ++j) {
tchecker::clock_id_t second_cur = j + orig_clocks_offset;
result.emplace_back(second_cur, cur, tchecker::dbm::access(this->dbm(), this->dim(), j, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), j, i)->value);
result.emplace_back(cur, second_cur, tchecker::dbm::access(this->dbm(), this->dim(), i, j)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, j)->value);
}
}
return result;
}
tchecker::zone_container_t<virtual_constraint_t> virtual_constraint_t::logic_and(tchecker::zone_container_t<virtual_constraint_t> *container)
{
tchecker::zone_container_t<virtual_constraint_t> result{this->dim()};
for(auto iter = container->begin(); iter < container->end(); iter++ ) {
std::shared_ptr<virtual_constraint_t> to_append = factory(this->dim());
if(tchecker::dbm::EMPTY != tchecker::dbm::intersection(to_append->dbm(), (*iter)->dbm(), this->dbm(), this->dim())) {
result.append_zone(to_append);
}
}
return result;
}
std::shared_ptr<virtual_constraint_t> factory(tchecker::clock_id_t dim)
{
return static_pointer_cast<tchecker::virtual_constraint::virtual_constraint_t>(
tchecker::zg::factory(dim));
}
std::shared_ptr<virtual_constraint_t> factory(tchecker::virtual_constraint::virtual_constraint_t const & virtual_constraint)
{
tchecker::zg::zone_t const & reinterpreted_zone = reinterpret_cast<tchecker::zg::zone_t const &>(virtual_constraint);
return static_pointer_cast<tchecker::virtual_constraint::virtual_constraint_t>(
tchecker::zg::factory(reinterpreted_zone)
);
}
std::shared_ptr<virtual_constraint_t> factory(std::shared_ptr<tchecker::zg::zone_t const> zone, tchecker::clock_id_t no_of_virtual_clocks)
{
return factory(zone->dbm(), zone->dim(), no_of_virtual_clocks);
}
std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virtual_clocks)
{
std::shared_ptr<virtual_constraint_t> result = factory(no_of_virtual_clocks + 1);
std::vector<tchecker::clock_id_t> indices;
indices.emplace_back(0);
for(tchecker::clock_id_t i = dim - no_of_virtual_clocks; i < dim; ++i)
{
indices.emplace_back(i);
}
for(std::size_t i = 0; i < indices.size(); ++i)
{
for(std::size_t j = 0; j < indices.size(); ++j)
{
tchecker::dbm::constrain(
result->dbm(), result->dim(), i, j, dbm[indices[i]*dim + indices[j]].cmp, dbm[indices[i]*dim + indices[j]].value
);
}
}
return result;
}
void destruct(virtual_constraint_t *to_destruct)
{
tchecker::zg::zone_destruct_and_deallocate(to_destruct);
}
tchecker::zone_container_t<virtual_constraint_t> * combine_lhs_land_not_rhs(std::shared_ptr<virtual_constraint_t> lhs, std::shared_ptr<virtual_constraint_t> rhs, tchecker::clock_id_t dim)
{
tchecker::zone_container_t<virtual_constraint_t> *result = new tchecker::zone_container_t<virtual_constraint_t>(dim);
tchecker::zone_container_t<virtual_constraint_t> *neg = rhs->neg();
for(auto iter = neg->begin(); iter < neg->end(); iter++) {
std::shared_ptr<virtual_constraint_t> to_append = factory(dim);
if(tchecker::dbm::EMPTY != tchecker::dbm::intersection(to_append->dbm(), (*iter)->dbm(), lhs->dbm(), dim)) {
result->append_zone(*to_append); // to_append is copied here
}
destruct(&(*to_append));
}
return result;
}
tchecker::zone_container_t<virtual_constraint_t> * combine_helper(std::shared_ptr<virtual_constraint_t> lhs, tchecker::zone_container_t<virtual_constraint_t> * lo_vc, tchecker::clock_id_t dim)
{
tchecker::zone_container_t<virtual_constraint_t> *result = new tchecker::zone_container_t<virtual_constraint_t>(dim);
result->append_zone(*lhs);
for(auto iter = lo_vc->begin(); iter < lo_vc->end(); iter++) {
tchecker::zone_container_t<virtual_constraint_t> *inter = result;
result = new tchecker::zone_container_t<virtual_constraint_t>(dim);
for(auto inter_iter = inter->begin(); inter_iter < inter->end(); inter_iter++) {
tchecker::zone_container_t<virtual_constraint_t> *lhs_land_not_rhs = combine_lhs_land_not_rhs(*inter_iter, *iter, dim);
for(auto land_iter = lhs_land_not_rhs->begin(); land_iter < lhs_land_not_rhs->end(); land_iter++) {
result->append_zone(*land_iter);
}
}
delete inter;
}
return result;
}
tchecker::zone_container_t<virtual_constraint_t> * combine(std::vector<tchecker::zone_container_t<virtual_constraint_t>> & lo_lo_vc, tchecker::clock_id_t dim)
{
if(lo_lo_vc.empty()) {
return new tchecker::zone_container_t<virtual_constraint_t>(dim);
}
tchecker::zone_container_t<virtual_constraint_t> cur = lo_lo_vc.back();
lo_lo_vc.pop_back();
tchecker::zone_container_t<virtual_constraint_t> *result = combine(lo_lo_vc, dim);
for(auto cur_iter = cur.begin(); cur_iter < cur.end(); cur_iter++) {
tchecker::zone_container_t<virtual_constraint_t> *inter = combine_helper(*cur_iter, result, dim);
delete result;
result = inter;
}
return result;
}
} // end of namespace virtual_constraint
} // end of namespace tchecker

2
src/zg/CMakeLists.txt
View file

@ -3,7 +3,6 @@
# See files AUTHORS and LICENSE for copyright details.
set(ZG_SRC
${CMAKE_CURRENT_SOURCE_DIR}/extrapolation.cc
${CMAKE_CURRENT_SOURCE_DIR}/path.cc
${CMAKE_CURRENT_SOURCE_DIR}/semantics.cc
${CMAKE_CURRENT_SOURCE_DIR}/state.cc
@ -11,7 +10,6 @@ ${CMAKE_CURRENT_SOURCE_DIR}/transition.cc
${CMAKE_CURRENT_SOURCE_DIR}/zg.cc
${CMAKE_CURRENT_SOURCE_DIR}/zone.cc
${TCHECKER_INCLUDE_DIR}/tchecker/zg/allocators.hh
${TCHECKER_INCLUDE_DIR}/tchecker/zg/extrapolation.hh
${TCHECKER_INCLUDE_DIR}/tchecker/zg/path.hh
${TCHECKER_INCLUDE_DIR}/tchecker/zg/semantics.hh
${TCHECKER_INCLUDE_DIR}/tchecker/zg/state.hh

264
src/zg/extrapolation.cc
View file

@ -1,264 +0,0 @@
/*
* This file is a part of the TChecker project.
*
* See files AUTHORS and LICENSE for copyright details.
*
*/
#include "tchecker/zg/extrapolation.hh"
#include "tchecker/clockbounds/solver.hh"
namespace tchecker {
namespace zg {
/* no_extrapolation_t */
void no_extrapolation_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) {}
/* global_lu_extrapolation_t */
namespace details {
global_lu_extrapolation_t::global_lu_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds)
: _clock_bounds(clock_bounds)
{
}
} // end of namespace details
/* global_extra_lu_t */
void global_extra_lu_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_lu(dbm, dim, _clock_bounds->L().ptr(), _clock_bounds->U().ptr());
}
/* global_extra_lu_plus_t */
void global_extra_lu_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_lu_plus(dbm, dim, _clock_bounds->L().ptr(), _clock_bounds->U().ptr());
}
/* local_lu_extrapolation_t */
namespace details {
local_lu_extrapolation_t::local_lu_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::local_lu_map_t const> const & clock_bounds)
: _l(nullptr), _u(nullptr), _clock_bounds(clock_bounds)
{
_l = tchecker::clockbounds::allocate_map(_clock_bounds->clock_number());
_u = tchecker::clockbounds::allocate_map(_clock_bounds->clock_number());
}
local_lu_extrapolation_t::local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t const & e)
: _clock_bounds(e._clock_bounds)
{
_l = tchecker::clockbounds::clone_map(*e._l);
_u = tchecker::clockbounds::clone_map(*e._u);
}
local_lu_extrapolation_t::local_lu_extrapolation_t(tchecker::zg::details::local_lu_extrapolation_t && e)
: _l(std::move(e._l)), _u(std::move(e._u)), _clock_bounds(std::move(e._clock_bounds))
{
e._l = nullptr;
e._u = nullptr;
}
local_lu_extrapolation_t::~local_lu_extrapolation_t()
{
tchecker::clockbounds::deallocate_map(_l);
tchecker::clockbounds::deallocate_map(_u);
}
tchecker::zg::details::local_lu_extrapolation_t &
local_lu_extrapolation_t::operator=(tchecker::zg::details::local_lu_extrapolation_t const & e)
{
if (this != &e) {
_clock_bounds = e._clock_bounds;
tchecker::clockbounds::deallocate_map(_l);
_l = tchecker::clockbounds::clone_map(*e._l);
tchecker::clockbounds::deallocate_map(_u);
_u = tchecker::clockbounds::clone_map(*e._u);
}
return *this;
}
tchecker::zg::details::local_lu_extrapolation_t &
local_lu_extrapolation_t::operator=(tchecker::zg::details::local_lu_extrapolation_t && e)
{
if (this != &e) {
_clock_bounds = std::move(e._clock_bounds);
_l = std::move(e._l);
_u = std::move(e._u);
e._l = nullptr;
e._u = nullptr;
}
return *this;
}
} // end of namespace details
/* local_extra_lu_t */
void local_extra_lu_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_l, *_u);
tchecker::dbm::extra_lu(dbm, dim, _l->ptr(), _u->ptr());
}
/* local_extra_lu_plus_t */
void local_extra_lu_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_l, *_u);
tchecker::dbm::extra_lu_plus(dbm, dim, _l->ptr(), _u->ptr());
}
/* global_m_extrapolation_t */
namespace details {
global_m_extrapolation_t::global_m_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::global_m_map_t const> const & clock_bounds)
: _clock_bounds(clock_bounds)
{
}
} // end of namespace details
/* global_extra_m_t */
void global_extra_m_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_m(dbm, dim, _clock_bounds->M().ptr());
}
/* global_extra_m_plus_t */
void global_extra_m_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
tchecker::dbm::extra_m_plus(dbm, dim, _clock_bounds->M().ptr());
}
/* local_m_extrapolation_t */
namespace details {
local_m_extrapolation_t::local_m_extrapolation_t(
std::shared_ptr<tchecker::clockbounds::local_m_map_t const> const & clock_bounds)
: _m(nullptr), _clock_bounds(clock_bounds)
{
_m = tchecker::clockbounds::allocate_map(_clock_bounds->clock_number());
}
local_m_extrapolation_t::local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t const & e)
: _m(nullptr), _clock_bounds(e._clock_bounds)
{
_m = tchecker::clockbounds::clone_map(*e._m);
}
local_m_extrapolation_t::local_m_extrapolation_t(tchecker::zg::details::local_m_extrapolation_t && e)
: _m(std::move(e._m)), _clock_bounds(std::move(e._clock_bounds))
{
e._m = nullptr;
}
local_m_extrapolation_t::~local_m_extrapolation_t() { tchecker::clockbounds::deallocate_map(_m); }
tchecker::zg::details::local_m_extrapolation_t &
local_m_extrapolation_t::operator=(tchecker::zg::details::local_m_extrapolation_t const & e)
{
if (this != &e) {
tchecker::clockbounds::deallocate_map(_m);
_m = tchecker::clockbounds::clone_map(*e._m);
_clock_bounds = e._clock_bounds;
}
return *this;
}
tchecker::zg::details::local_m_extrapolation_t &
local_m_extrapolation_t::operator=(tchecker::zg::details::local_m_extrapolation_t && e)
{
if (this != &e) {
_m = std::move(e._m);
e._m = nullptr;
_clock_bounds = std::move(e._clock_bounds);
}
return *this;
}
} // namespace details
/* local_extra_m_t */
void local_extra_m_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_m);
tchecker::dbm::extra_m(dbm, dim, _m->ptr());
}
/* local_extra_m_plus_t */
void local_extra_m_plus_t::extrapolate(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc)
{
assert(dim == _clock_bounds->clock_number() + 1);
_clock_bounds->bounds(vloc, *_m);
tchecker::dbm::extra_m_plus(dbm, dim, _m->ptr());
}
/* factories */
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::ta::system_t const & system)
{
if (extrapolation_type == tchecker::zg::NO_EXTRAPOLATION)
return new tchecker::zg::no_extrapolation_t;
std::unique_ptr<tchecker::clockbounds::clockbounds_t> clock_bounds{tchecker::clockbounds::compute_clockbounds(system)};
if (clock_bounds.get() == nullptr)
return nullptr;
return tchecker::zg::extrapolation_factory(extrapolation_type, *clock_bounds);
}
tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t extrapolation_type,
tchecker::clockbounds::clockbounds_t const & clock_bounds)
{
if (extrapolation_type == tchecker::zg::NO_EXTRAPOLATION)
return new tchecker::zg::no_extrapolation_t;
switch (extrapolation_type) {
case tchecker::zg::EXTRA_LU_GLOBAL:
return new tchecker::zg::global_extra_lu_t{clock_bounds.global_lu_map()};
case tchecker::zg::EXTRA_LU_LOCAL:
return new tchecker::zg::local_extra_lu_t{clock_bounds.local_lu_map()};
case tchecker::zg::EXTRA_LU_PLUS_GLOBAL:
return new tchecker::zg::global_extra_lu_plus_t{clock_bounds.global_lu_map()};
case tchecker::zg::EXTRA_LU_PLUS_LOCAL:
return new tchecker::zg::local_extra_lu_plus_t{clock_bounds.local_lu_map()};
case tchecker::zg::EXTRA_M_GLOBAL:
return new tchecker::zg::global_extra_m_t{clock_bounds.global_m_map()};
case tchecker::zg::EXTRA_M_LOCAL:
return new tchecker::zg::local_extra_m_t{clock_bounds.local_m_map()};
case tchecker::zg::EXTRA_M_PLUS_GLOBAL:
return new tchecker::zg::global_extra_m_plus_t{clock_bounds.global_m_map()};
case tchecker::zg::EXTRA_M_PLUS_LOCAL:
return new tchecker::zg::local_extra_m_plus_t{clock_bounds.local_m_map()};
default:
throw std::invalid_argument("Unknown zone extrapolation");
}
}
} // end of namespace zg
} // end of namespace tchecker

8
src/zg/path.cc
View file

@ -136,7 +136,9 @@ tchecker::zg::path::symbolic::finite_path_t * compute_finite_path(std::shared_pt
{
tchecker::zg::path::symbolic::finite_path_t * path = new tchecker::zg::path::symbolic::finite_path_t{zg};
tchecker::zg::const_state_sptr_t s{tchecker::zg::initial(*zg, initial_vloc)};
tchecker::zg::const_state_sptr_t s{
tchecker::zg::initial(*zg, initial_vloc)};
if (s.ptr() == nullptr) {
delete path;
throw std::invalid_argument("*** compute_finite_path(symbolic): no initial state with given tuple of locations");
@ -200,7 +202,9 @@ compute_lasso_path(std::shared_ptr<tchecker::zg::zg_t> const & zg, tchecker::vlo
tchecker::zg::path::symbolic::lasso_path_t * path = new tchecker::zg::path::symbolic::lasso_path_t{zg};
// add initial node
tchecker::zg::const_state_sptr_t s{tchecker::zg::initial(*zg, initial_vloc)};
tchecker::zg::const_state_sptr_t s{
tchecker::zg::initial(*zg, initial_vloc)};
if (s.ptr() == nullptr) {
delete path;
throw std::invalid_argument("*** compute_lasso_path: no initial state with given tuple of locations");

106
src/zg/semantics.cc
View file

@ -12,10 +12,10 @@ namespace tchecker {
namespace zg {
/* standard_semantics_t */
/* helping functions to reduce copy paste code */
tchecker::state_status_t standard_semantics_t::initial(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
tchecker::state_status_t initial_helper(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
{
tchecker::dbm::zero(dbm, dim);
@ -25,8 +25,8 @@ tchecker::state_status_t standard_semantics_t::initial(tchecker::dbm::db_t * dbm
return tchecker::STATE_OK;
}
tchecker::state_status_t standard_semantics_t::final(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
tchecker::state_status_t final_helper(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
{
tchecker::dbm::universal_positive(dbm, dim);
@ -36,7 +36,7 @@ tchecker::state_status_t standard_semantics_t::final(tchecker::dbm::db_t * dbm,
return tchecker::STATE_OK;
}
tchecker::state_status_t standard_semantics_t::next(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::state_status_t next_helper(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
@ -63,11 +63,12 @@ tchecker::state_status_t standard_semantics_t::next(tchecker::dbm::db_t * dbm, t
return tchecker::STATE_OK;
}
tchecker::state_status_t standard_semantics_t::prev(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant)
tchecker::state_status_t prev_helper(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant)
{
// prev(dbm) = free_clocks(dbm & tgt_invariant & constraints(clkreset), left_clocks(clkreset)) & guard & src_invariant
// finally, if src_delay_allowed: opened down and intersected with src_invariant again
@ -97,6 +98,38 @@ tchecker::state_status_t standard_semantics_t::prev(tchecker::dbm::db_t * dbm, t
return tchecker::STATE_OK;
}
/* standard_semantics_t */
tchecker::state_status_t standard_semantics_t::initial(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
{
return initial_helper(dbm, dim, delay_allowed, invariant);
}
tchecker::state_status_t standard_semantics_t::final(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
{
return final_helper(dbm, dim, delay_allowed, invariant);
}
tchecker::state_status_t standard_semantics_t::next(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant)
{
return next_helper(dbm, dim, src_delay_allowed, src_invariant, guard, clkreset, tgt_delay_allowed, tgt_invariant);
}
tchecker::state_status_t standard_semantics_t::prev(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant)
{
return prev_helper(dbm, dim, src_delay_allowed, src_invariant, guard, clkreset, tgt_delay_allowed, tgt_invariant);
}
/* elapsed_semantics_t */
tchecker::state_status_t elapsed_semantics_t::initial(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
@ -187,6 +220,53 @@ tchecker::state_status_t elapsed_semantics_t::prev(tchecker::dbm::db_t * dbm, tc
return tchecker::STATE_OK;
}
/* distinguished_semantics_t */
tchecker::state_status_t distinguished_semantics_t::initial( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
{
return initial_helper(dbm, dim, delay_allowed, invariant);
}
tchecker::state_status_t distinguished_semantics_t::final( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
tchecker::clock_constraint_container_t const & invariant)
{
return final_helper(dbm, dim, delay_allowed, invariant);
}
tchecker::state_status_t distinguished_semantics_t::delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim,
tchecker::clock_constraint_container_t const & invariant)
{
if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY)
return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED;
tchecker::dbm::open_up(dbm, dim);
if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY)
return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; // should never occur
return tchecker::STATE_OK;
}
tchecker::state_status_t distinguished_semantics_t::next( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant)
{
return next_helper(dbm, dim, false, src_invariant, guard, clkreset, false, tgt_invariant);
}
tchecker::state_status_t distinguished_semantics_t::prev( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,
tchecker::clock_constraint_container_t const & src_invariant,
tchecker::clock_constraint_container_t const & guard,
tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
tchecker::clock_constraint_container_t const & tgt_invariant)
{
return prev_helper(dbm, dim, false, src_invariant, guard, clkreset, false, tgt_invariant);
}
/* factory */
tchecker::zg::semantics_t * semantics_factory(enum semantics_type_t semantics)
@ -196,6 +276,8 @@ tchecker::zg::semantics_t * semantics_factory(enum semantics_type_t semantics)
return new tchecker::zg::standard_semantics_t{};
case tchecker::zg::ELAPSED_SEMANTICS:
return new tchecker::zg::elapsed_semantics_t{};
case tchecker::zg::DISTINGUISHED_SEMANTICS:
return new tchecker::zg::distinguished_semantics_t{};
default:
throw std::invalid_argument("Unknown zone semantics");
}
@ -203,4 +285,4 @@ tchecker::zg::semantics_t * semantics_factory(enum semantics_type_t semantics)
} // end of namespace zg
} // end of namespace tchecker
} // end of namespace tchecker

504
src/zg/zg.cc
View file

@ -5,330 +5,167 @@
*
*/
#include "tchecker/zg/zg.hh"
#include <queue>
#include "tchecker/dbm/db.hh"
#include "tchecker/variables/clocks.hh"
#include "tchecker/zg/zg.hh"
/* zg_t public functions */
namespace tchecker {
namespace zg {
/* Semantics functions */
tchecker::state_status_t initial(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation,
tchecker::zg::initial_value_t const & initial_range)
initial_range_t zg_t::initial_edges()
{
tchecker::state_status_t status = tchecker::ta::initial(system, vloc, intval, vedge, invariant, initial_range);
if (status != tchecker::STATE_OK)
return status;
tchecker::dbm::db_t * dbm = zone->dbm();
tchecker::clock_id_t dim = zone->dim();
bool delay_allowed = tchecker::ta::delay_allowed(system, *vloc);
status = semantics.initial(dbm, dim, delay_allowed, invariant);
if (status != tchecker::STATE_OK)
return status;
extrapolation.extrapolate(dbm, dim, *vloc);
return tchecker::STATE_OK;
return tchecker::ta::initial_edges(*_system);
}
tchecker::state_status_t final(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation, tchecker::zg::final_value_t const & final_range)
void zg_t::initial(initial_value_t const & init_edge, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
tchecker::state_status_t status = tchecker::ta::final(system, vloc, intval, vedge, invariant, final_range);
if (status != tchecker::STATE_OK)
return status;
auto ta_func = [](auto system, auto s, auto t, auto edge, auto unused) {
return tchecker::ta::initial(system, s->vloc_ptr(), s->intval_ptr(),
t->vedge_ptr(), t->src_invariant_container(), edge);
};
tchecker::dbm::db_t * dbm = zone->dbm();
tchecker::clock_id_t dim = zone->dim();
bool delay_allowed = tchecker::ta::delay_allowed(system, *vloc);
auto se_func = [](auto system, auto semantics, auto dbm, auto dim, auto s, auto t, auto unused) {
bool delay_allowed = tchecker::ta::delay_allowed(system, *(s->vloc_ptr()));
return semantics.initial(dbm, dim, delay_allowed, t->src_invariant_container());
};
status = semantics.final(dbm, dim, delay_allowed, invariant);
if (status != tchecker::STATE_OK)
return status;
extrapolation.extrapolate(dbm, dim, *vloc);
return tchecker::STATE_OK;
sst_handler<initial_value_t const, bool>(init_edge, v, mask, ta_func, se_func, nullptr, false);
}
tchecker::state_status_t next(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & src_invariant,
tchecker::clock_constraint_container_t & guard, tchecker::clock_reset_container_t & reset,
tchecker::clock_constraint_container_t & tgt_invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation, tchecker::zg::outgoing_edges_value_t const & edges)
void zg_t::initial(std::vector<sst_t> & v, tchecker::state_status_t mask)
{
bool src_delay_allowed = tchecker::ta::delay_allowed(system, *vloc);
tchecker::state_status_t status =
tchecker::ta::next(system, vloc, intval, vedge, src_invariant, guard, reset, tgt_invariant, edges);
if (status != tchecker::STATE_OK)
return status;
tchecker::dbm::db_t * dbm = zone->dbm();
tchecker::clock_id_t dim = zone->dim();
bool tgt_delay_allowed = tchecker::ta::delay_allowed(system, *vloc);
status = semantics.next(dbm, dim, src_delay_allowed, src_invariant, guard, reset, tgt_delay_allowed, tgt_invariant);
if (status != tchecker::STATE_OK)
return status;
extrapolation.extrapolate(dbm, dim, *vloc);
return tchecker::STATE_OK;
tchecker::ts::initial(*this, v, mask);
}
tchecker::state_status_t prev(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & src_invariant,
tchecker::clock_constraint_container_t & guard, tchecker::clock_reset_container_t & reset,
tchecker::clock_constraint_container_t & tgt_invariant, tchecker::zg::semantics_t & semantics,
tchecker::zg::extrapolation_t & extrapolation, tchecker::zg::incoming_edges_value_t const & edges)
outgoing_edges_range_t zg_t::outgoing_edges(tchecker::zg::const_state_sptr_t const & s)
{
bool tgt_delay_allowed = tchecker::ta::delay_allowed(system, *vloc);
tchecker::state_status_t status =
tchecker::ta::prev(system, vloc, intval, vedge, src_invariant, guard, reset, tgt_invariant, edges);
if (status != tchecker::STATE_OK)
return status;
tchecker::dbm::db_t * dbm = zone->dbm();
tchecker::clock_id_t dim = zone->dim();
bool src_delay_allowed = tchecker::ta::delay_allowed(system, *vloc);
status = semantics.prev(dbm, dim, src_delay_allowed, src_invariant, guard, reset, tgt_delay_allowed, tgt_invariant);
if (status != tchecker::STATE_OK)
return status;
extrapolation.extrapolate(dbm, dim, *vloc);
return tchecker::STATE_OK;
return tchecker::ta::outgoing_edges(*_system, s->vloc_ptr());
}
/* labels */
boost::dynamic_bitset<> labels(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s)
void zg_t::next(tchecker::zg::const_state_sptr_t const & s, outgoing_edges_value_t const & out_edge, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
return tchecker::ta::labels(system, s);
auto ta_func = [](auto system, auto s, auto t, auto edge, auto src_delay) {
*src_delay = tchecker::ta::delay_allowed(system, *(s->vloc_ptr()));
return tchecker::ta::next(system, s->vloc_ptr(), s->intval_ptr(),
t->vedge_ptr(), t->src_invariant_container(), t->guard_container(),
t->reset_container(), t->tgt_invariant_container(), edge);
};
auto se_func = []( auto system, auto semantics, auto dbm, auto dim, auto s, auto t, auto src_delay) {
bool tgt_delay = tchecker::ta::delay_allowed(system, *(s->vloc_ptr()));
return semantics.next(dbm, dim, *src_delay, t->src_invariant_container(), t->guard_container(),
t->reset_container(), tgt_delay, t->tgt_invariant_container());
};
sst_handler<outgoing_edges_value_t const, bool>(out_edge, v, mask, ta_func, se_func, s, true);
}
/* is_valid_final */
bool is_valid_final(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s) { return !s.zone().is_empty(); }
/* is_initial */
bool is_initial(tchecker::ta::system_t const & system, tchecker::zg::zone_t const & zone)
{
assert(zone.dim() == system.clocks_count(tchecker::VK_FLATTENED) + 1);
return tchecker::dbm::contains_zero(zone.dbm(), zone.dim());
}
bool is_initial(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s)
{
return tchecker::ta::is_initial(system, s) && tchecker::zg::is_initial(system, s.zone());
}
/* attributes */
void attributes(tchecker::ta::system_t const & system, tchecker::zg::state_t const & s, std::map<std::string, std::string> & m)
{
tchecker::ta::attributes(system, s, m);
m["zone"] = tchecker::to_string(s.zone(), system.clock_variables().flattened().index());
}
void attributes(tchecker::ta::system_t const & system, tchecker::zg::transition_t const & t,
std::map<std::string, std::string> & m)
{
tchecker::ta::attributes(system, t, m);
}
/* initialize */
tchecker::state_status_t initialize(tchecker::ta::system_t const & system,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vloc_t> const & vloc,
tchecker::intrusive_shared_ptr_t<tchecker::shared_intval_t> const & intval,
tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> const & zone,
tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t> const & vedge,
tchecker::clock_constraint_container_t & invariant,
std::map<std::string, std::string> const & attributes)
{
// initialize vloc, intval and vedge from ta
auto state_status = tchecker::ta::initialize(system, vloc, intval, vedge, invariant, attributes);
if (state_status != STATE_OK)
return state_status;
// initialize zone from attributes["zone"]
tchecker::clock_constraint_container_t clk_constraints;
try {
tchecker::from_string(clk_constraints, system.clock_variables(), attributes.at("zone"));
}
catch (...) {
return tchecker::STATE_BAD;
}
tchecker::dbm::db_t * dbm = zone->dbm();
tchecker::clock_id_t const dim = zone->dim();
tchecker::dbm::universal_positive(dbm, dim);
tchecker::dbm::status_t zone_status = tchecker::dbm::constrain(dbm, dim, clk_constraints);
if (zone_status == tchecker::dbm::EMPTY)
return tchecker::STATE_BAD;
// Apply invariant
zone_status = tchecker::dbm::constrain(dbm, dim, invariant);
if (zone_status == tchecker::dbm::EMPTY)
return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED;
return tchecker::STATE_OK;
}
/* zg_t */
zg_t::zg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
std::shared_ptr<tchecker::zg::semantics_t> const & semantics,
std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size)
: _system(system), _sharing_type(sharing_type), _semantics(semantics), _extrapolation(extrapolation),
_state_allocator(block_size, block_size, _system->processes_count(), block_size,
_system->intvars_count(tchecker::VK_FLATTENED), block_size,
_system->clocks_count(tchecker::VK_FLATTENED) + 1, table_size),
_transition_allocator(block_size, block_size, _system->processes_count(), table_size)
{
}
initial_range_t zg_t::initial_edges() { return tchecker::zg::initial_edges(*_system); }
void zg_t::initial(tchecker::zg::initial_value_t const & init_edge, std::vector<sst_t> & v, tchecker::state_status_t mask)
{
tchecker::zg::state_sptr_t s = _state_allocator.construct();
tchecker::zg::transition_sptr_t t = _transition_allocator.construct();
tchecker::state_status_t status = tchecker::zg::initial(*_system, *s, *t, *_semantics, *_extrapolation, init_edge);
if (status & mask) {
if (_sharing_type == tchecker::ts::SHARING) {
share(s);
share(t);
}
v.push_back(std::make_tuple(status, s, t));
}
}
void zg_t::initial(std::vector<sst_t> & v, tchecker::state_status_t mask) { tchecker::ts::initial(*this, v, mask); }
tchecker::zg::outgoing_edges_range_t zg_t::outgoing_edges(tchecker::zg::const_state_sptr_t const & s)
{
return tchecker::zg::outgoing_edges(*_system, s->vloc_ptr());
}
void zg_t::next(tchecker::zg::const_state_sptr_t const & s, tchecker::zg::outgoing_edges_value_t const & out_edge,
std::vector<sst_t> & v, tchecker::state_status_t mask)
{
tchecker::zg::state_sptr_t nexts = _state_allocator.clone(*s);
tchecker::zg::transition_sptr_t nextt = _transition_allocator.construct();
tchecker::state_status_t status = tchecker::zg::next(*_system, *nexts, *nextt, *_semantics, *_extrapolation, out_edge);
if (status & mask) {
if (_sharing_type == tchecker::ts::SHARING) {
share(nexts);
share(nextt);
}
v.push_back(std::make_tuple(status, nexts, nextt));
}
}
void zg_t::next(tchecker::zg::const_state_sptr_t const & s, std::vector<sst_t> & v, tchecker::state_status_t mask)
void zg_t::next(tchecker::zg::const_state_sptr_t const & s, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
tchecker::ts::next(*this, s, v, mask);
}
// Backward
final_range_t zg_t::final_edges(boost::dynamic_bitset<> const & labels) { return tchecker::zg::final_edges(*_system, labels); }
void zg_t::final(final_value_t const & final_edge, std::vector<sst_t> & v, tchecker::state_status_t mask)
final_range_t zg_t::final_edges(boost::dynamic_bitset<> const & labels)
{
tchecker::zg::state_sptr_t s = _state_allocator.construct();
tchecker::zg::transition_sptr_t t = _transition_allocator.construct();
tchecker::state_status_t status = tchecker::zg::final(*_system, *s, *t, *_semantics, *_extrapolation, final_edge);
if (status & mask) {
if (_sharing_type == tchecker::ts::SHARING) {
share(s);
share(t);
}
v.push_back(std::make_tuple(status, s, t));
}
return tchecker::ta::final_edges(*_system, labels);
}
void zg_t::final(boost::dynamic_bitset<> const & labels, std::vector<sst_t> & v, tchecker::state_status_t mask)
void zg_t::final(final_value_t const & final_edge, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
auto ta_func = [](auto system, auto s, auto t, auto edge, auto unused) {
return tchecker::ta::final(system, s->vloc_ptr(), s->intval_ptr(),
t->vedge_ptr(), t->src_invariant_container(), edge);
};
auto se_func = []( auto system, auto semantics, auto dbm, auto dim, auto s, auto t, auto unused) {
bool delay = tchecker::ta::delay_allowed(system, *(s->vloc_ptr()));
return semantics.final(dbm, dim, delay, t->src_invariant_container());
};
sst_handler<final_value_t const, bool>(final_edge, v, mask, ta_func, se_func, nullptr, false);
}
void zg_t::final(boost::dynamic_bitset<> const & labels, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
tchecker::ts::final(*this, labels, v, mask);
}
incoming_edges_range_t zg_t::incoming_edges(tchecker::zg::const_state_sptr_t const & s)
{
return tchecker::zg::incoming_edges(*_system, s->vloc_ptr());
return tchecker::ta::incoming_edges(*_system, s->vloc_ptr());
}
void zg_t::prev(tchecker::zg::const_state_sptr_t const & s, incoming_edges_value_t const & in_edge, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
tchecker::zg::state_sptr_t prevs = _state_allocator.clone(*s);
tchecker::zg::transition_sptr_t prevt = _transition_allocator.construct();
tchecker::state_status_t status = tchecker::zg::prev(*_system, *prevs, *prevt, *_semantics, *_extrapolation, in_edge);
if (status & mask) {
if (_sharing_type == tchecker::ts::SHARING) {
share(prevs);
share(prevt);
}
v.push_back(std::make_tuple(status, prevs, prevt));
}
auto ta_func = [](auto system, auto s, auto t, auto edge, auto tgt_delay) {
*tgt_delay = tchecker::ta::delay_allowed(system, *(s->vloc_ptr()));
return tchecker::ta::prev(system, s->vloc_ptr(), s->intval_ptr(), t->vedge_ptr(),
t->src_invariant_container(), t->guard_container(),
t->reset_container(), t->tgt_invariant_container(), edge);
};
auto se_func = []( auto system, auto semantics, auto dbm, auto dim, auto s, auto t, auto tgt_delay) {
bool src_delay = tchecker::ta::delay_allowed(system, *(s->vloc_ptr()));
return semantics.prev(dbm, dim, src_delay, t->src_invariant_container(), t->guard_container(),
t->reset_container(), *tgt_delay, t->tgt_invariant_container());
};
sst_handler<incoming_edges_value_t const, bool>(in_edge, v, mask, ta_func, se_func, s, true);
}
void zg_t::prev(tchecker::zg::const_state_sptr_t const & s, std::vector<sst_t> & v, tchecker::state_status_t mask)
void zg_t::prev(tchecker::zg::const_state_sptr_t const & s, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
tchecker::ts::prev(*this, s, v, mask);
}
// Builder
void zg_t::build(std::map<std::string, std::string> const & attributes, std::vector<sst_t> & v, tchecker::state_status_t mask)
void zg_t::build(std::map<std::string, std::string> const & attributes, std::vector<sst_t> & v,
tchecker::state_status_t mask)
{
tchecker::zg::state_sptr_t s = _state_allocator.construct();
tchecker::zg::transition_sptr_t t = _transition_allocator.construct();
tchecker::state_status_t status = tchecker::zg::initialize(*_system, *s, *t, attributes);
if (status & mask) {
if (_sharing_type == tchecker::ts::SHARING) {
share(s);
share(t);
}
v.push_back(std::make_tuple(status, s, t));
}
auto ta_func = [](auto system, auto s, auto t, auto attributes, auto clk_constraints) {
auto state_status = tchecker::ta::initialize(system, s->vloc_ptr(), s->intval_ptr(),
t->vedge_ptr(), t->src_invariant_container(), attributes);
if (state_status != STATE_OK)
return state_status;
// initialize zone from attributes["zone"]
try {
tchecker::from_string(*clk_constraints, system.clock_variables(), attributes.at("zone"));
}
catch (...) {
return tchecker::STATE_BAD;
}
return tchecker::STATE_OK;
};
auto se_func = [](auto system, auto semantics, auto dbm, auto dim, auto s, auto t, auto clk_constraints) {
tchecker::dbm::universal_positive(dbm, dim);
tchecker::dbm::status_t zone_status = tchecker::dbm::constrain(dbm, dim, *clk_constraints);
if (zone_status == tchecker::dbm::EMPTY)
return tchecker::STATE_BAD;
// Apply invariant
zone_status = tchecker::dbm::constrain(dbm, dim, t->src_invariant_container());
if (zone_status == tchecker::dbm::EMPTY)
return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED;
return tchecker::STATE_OK;
};
sst_handler<std::map<std::string, std::string> const &, tchecker::clock_constraint_container_t>(attributes, v, mask, ta_func, se_func, nullptr, false);
}
// Split
void zg_t::split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_constraint_t const & c,
std::vector<tchecker::zg::state_sptr_t> & v)
std::vector<tchecker::zg::state_sptr_t> & v)
{
if (!tchecker::dbm::satisfies(s->zone().dbm(), s->zone().dim(), c))
v.push_back(clone_and_constrain(s, -c));
@ -337,7 +174,7 @@ void zg_t::split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_con
}
void zg_t::split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_constraint_container_t const & constraints,
std::vector<tchecker::zg::state_sptr_t> & v)
std::vector<tchecker::zg::state_sptr_t> & v)
{
std::vector<tchecker::zg::state_sptr_t> done;
std::queue<tchecker::zg::state_sptr_t> todo;
@ -357,37 +194,97 @@ void zg_t::split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_con
v.push_back(todo.front());
}
// Inspector
boost::dynamic_bitset<> zg_t::labels(tchecker::zg::const_state_sptr_t const & s) const
{
return tchecker::zg::labels(*_system, *s);
return tchecker::ta::labels(*_system, *s);
}
void zg_t::attributes(tchecker::zg::const_state_sptr_t const & s, std::map<std::string, std::string> & m) const
{
tchecker::zg::attributes(*_system, *s, m);
tchecker::ta::attributes(*_system, *s, m);
m["zone"] = tchecker::to_string(s->zone(), _system->clock_variables().flattened().index());
}
void zg_t::attributes(tchecker::zg::const_transition_sptr_t const & t, std::map<std::string, std::string> & m) const
{
tchecker::zg::attributes(*_system, *t, m);
tchecker::ta::attributes(*_system, *t, m);
}
bool zg_t::is_valid_final(tchecker::zg::const_state_sptr_t const & s) const
{
return tchecker::zg::is_valid_final(*_system, *s);
return !s->zone().is_empty();
}
bool zg_t::is_initial(tchecker::zg::const_state_sptr_t const & s) const { return tchecker::zg::is_initial(*_system, *s); }
bool zg_t::is_initial(tchecker::zg::const_state_sptr_t const & s) const
{
assert(s->zone_ptr()->dim() == _system->clocks_count(tchecker::VK_FLATTENED) + 1);
return tchecker::ta::is_initial(*_system, *s) && tchecker::dbm::contains_zero(s->zone_ptr()->dbm(), s->zone_ptr()->dim());
}
// Sharing
void zg_t::share(tchecker::zg::state_sptr_t & s)
{
_state_allocator.share(s);
}
void zg_t::share(tchecker::zg::state_sptr_t & s) { _state_allocator.share(s); }
void zg_t::share(tchecker::zg::transition_sptr_t & t)
{
_transition_allocator.share(t);
}
/* zg_t private functions */
template<typename edge_t, typename helping_hand_t>
void zg_t::sst_handler( edge_t edge, std::vector<sst_t> & v, tchecker::state_status_t mask,
tchecker::state_status_t (*ta_func)(tchecker::ta::system_t const &,
tchecker::zg::state_sptr_t &,
tchecker::zg::transition_sptr_t &,
edge_t &,
helping_hand_t *),
tchecker::state_status_t (*se_func)( tchecker::ta::system_t const &,
tchecker::zg::semantics_t &,
tchecker::dbm::db_t *,
tchecker::clock_id_t,
tchecker::zg::state_sptr_t &,
tchecker::zg::transition_sptr_t &,
helping_hand_t *),
tchecker::zg::const_state_sptr_t const & to_clone, bool clone
)
{
tchecker::zg::state_sptr_t s;
if(clone) { // for some crazy reason, I cannot check for null here and, therefore, we need clone
s = _state_allocator.clone(*to_clone);
}
else {
s = _state_allocator.construct();
}
tchecker::zg::transition_sptr_t t = _transition_allocator.construct();
helping_hand_t helper;
tchecker::state_status_t status = ta_func(*_system, s, t, edge, &helper);
if(tchecker::STATE_OK == status) {
tchecker::dbm::db_t * dbm = s->zone_ptr()->dbm();
tchecker::clock_id_t dim = s->zone_ptr()->dim();
status = se_func(*_system, *_semantics, dbm, dim, s, t, &helper);
if(tchecker::STATE_OK == status) {
_extrapolation->extrapolate(dbm, dim, *(s->vloc_ptr()));
}
}
if (status & mask) {
if (_sharing_type == tchecker::ts::SHARING) {
share(s);
share(t);
}
v.push_back(std::make_tuple(status, s, t));
}
}
void zg_t::share(tchecker::zg::transition_sptr_t & t) { _transition_allocator.share(t); }
// Private
tchecker::zg::state_sptr_t zg_t::clone_and_constrain(tchecker::zg::const_state_sptr_t const & s,
tchecker::clock_constraint_t const & c)
@ -399,11 +296,27 @@ tchecker::zg::state_sptr_t zg_t::clone_and_constrain(tchecker::zg::const_state_s
return clone_s;
}
tchecker::zg::state_sptr_t zg_t::clone_and_constrain(tchecker::zg::const_state_sptr_t const & s,
clock_constraint_container_t const & c)
{
tchecker::zg::state_sptr_t clone_s = _state_allocator.clone(*s);
tchecker::dbm::constrain(clone_s->zone_ptr()->dbm(), clone_s->zone_ptr()->dim(), c);
if (!clone_s->zone().is_empty() && _sharing_type == tchecker::ts::SHARING)
share(clone_s);
return clone_s;
}
/* tools */
tchecker::zg::state_sptr_t initial(tchecker::zg::zg_t & zg, tchecker::vloc_t const & vloc, tchecker::state_status_t mask)
tchecker::zg::state_sptr_t
initial(tchecker::zg::zg_t & zg,
tchecker::vloc_t const & vloc, tchecker::state_status_t mask)
{
std::vector<tchecker::zg::zg_t::sst_t> v;
std::vector<typename tchecker::zg::zg_t::sst_t> v;
zg.initial(v, mask);
for (auto && [status, s, t] : v) {
if (s->vloc() == vloc)
@ -412,12 +325,11 @@ tchecker::zg::state_sptr_t initial(tchecker::zg::zg_t & zg, tchecker::vloc_t con
return nullptr;
}
std::tuple<tchecker::zg::state_sptr_t, tchecker::zg::transition_sptr_t> next(tchecker::zg::zg_t & zg,
tchecker::zg::const_state_sptr_t const & s,
tchecker::vedge_t const & vedge,
tchecker::state_status_t mask)
std::tuple<tchecker::zg::state_sptr_t, tchecker::zg::transition_sptr_t>
next(tchecker::zg::zg_t &zg,
tchecker::zg::const_state_sptr_t const & s, tchecker::vedge_t const & vedge, tchecker::state_status_t mask)
{
std::vector<tchecker::zg::zg_t::sst_t> v;
std::vector<typename tchecker::zg::zg_t::sst_t> v;
zg.next(s, v, mask);
for (auto && [status, nexts, nextt] : v)
if (nextt->vedge() == vedge)
@ -425,9 +337,11 @@ std::tuple<tchecker::zg::state_sptr_t, tchecker::zg::transition_sptr_t> next(tch
return std::make_tuple(nullptr, nullptr);
}
/* factory */
tchecker::zg::zg_t * factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size,
std::size_t table_size)
@ -437,10 +351,10 @@ tchecker::zg::zg_t * factory(std::shared_ptr<tchecker::ta::system_t const> const
if (extrapolation.get() == nullptr)
return nullptr;
std::shared_ptr<tchecker::zg::semantics_t> semantics{tchecker::zg::semantics_factory(semantics_type)};
return new tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size);
return std::make_shared<zg_t>(system, sharing_type, semantics, extrapolation, block_size, table_size);
}
tchecker::zg::zg_t * factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
enum tchecker::zg::extrapolation_type_t extrapolation_type,
tchecker::clockbounds::clockbounds_t const & clock_bounds, std::size_t block_size,
@ -451,7 +365,7 @@ tchecker::zg::zg_t * factory(std::shared_ptr<tchecker::ta::system_t const> const
if (extrapolation.get() == nullptr)
return nullptr;
std::shared_ptr<tchecker::zg::semantics_t> semantics{tchecker::zg::semantics_factory(semantics_type)};
return new tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size);
return std::make_shared<zg_t>(system, sharing_type, semantics, extrapolation, block_size, table_size);
}
} // end of namespace zg

13
src/zg/zone.cc
View file

@ -107,12 +107,25 @@ zone_t::~zone_t() = default;
// Allocation and deallocation
void zone_destruct_and_deallocate(tchecker::zg::zone_t * zone)
{
tchecker::zg::zone_t::destruct(zone);
delete[] reinterpret_cast<char *>(zone);
}
std::shared_ptr<zone_t> factory(tchecker::clock_id_t dim)
{
std::shared_ptr<zone_t> result(tchecker::zg::zone_allocate_and_construct(dim, dim), zone_destruct_and_deallocate);
return result;
}
std::shared_ptr<zone_t> factory(zone_t const & zone)
{
std::shared_ptr<zone_t> result(tchecker::zg::zone_allocate_and_construct(zone.dim(), zone), zone_destruct_and_deallocate);
return result;
}
} // end of namespace zg
std::string to_string(tchecker::zg::zone_t const & zone, tchecker::clock_index_t const & index)

6
test/CMakeLists.txt
View file

@ -8,8 +8,12 @@ include(${CMAKE_CURRENT_SOURCE_DIR}/TestUtils.cmake)
set(TCK_REACH "$<TARGET_FILE:tck-reach>")
set(TCK_REACH_SH "${CMAKE_CURRENT_SOURCE_DIR}/tck-reach.sh")
set(TCK_COMPARE "$<TARGET_FILE:tck-compare>")
set(TCK_COMPARE_SH "${CMAKE_CURRENT_SOURCE_DIR}/tck-compare.sh")
# Sub-directories to recurse into
set(SUBDIRS unit-tests bugfixes simple-nr algos)
set(SUBDIRS unit-tests bugfixes simple-nr algos tck-compare)
# Common script that redirects and checks outputs and errors generated by
# TChecker.

23
test/tck-compare.sh Executable file
View file

@ -0,0 +1,23 @@
#!/usr/bin/env bash
if ! test -n "${TCK_COMPARE}";
then
echo 1>&2 "missing variable TCK_COMPARE"
exit 1
fi
if ! test -n "${DOT_MAX_SIZE}";
then
DOT_MAX_SIZE=1000
fi
COMMAND="${TCK_COMPARE}"
while test $# != 0;
do
COMMAND="${COMMAND} $1"
shift
done
eval ${COMMAND} | sed -e 's/\(^MEMORY_MAX_RSS \).*$/\1 xxxx/g' -e 's/\(^RUNNING_TIME_SECONDS \).*$/\1 xxxx/g'
exit 0

78
test/tck-compare/CMakeLists.txt Normal file
View file

@ -0,0 +1,78 @@
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
# writing special register testcases function for tck-compare
# this is neccessary since the original register testcases function accepts a single
# input model only
function(create_testcase TEST_NAME first_input second_input relationship)
tck_add_test (${TEST_NAME} ${TEST_NAME} savelist)
set_tests_properties(${TEST_NAME}
PROPERTIES FIXTURES_REQUIRED "BUILD_TCK_COMPARE")
tck_add_test_envvar(testenv TCK_COMPARE "${TCK_COMPARE}")
tck_add_test_envvar(testenv TEST "${TCK_COMPARE_SH}")
tck_add_test_envvar(testenv TEST_ARGS "-r ${relationship} ${first_input} ${second_input}")
tck_add_test_envvar(testenv DOT_MAX_SIZE "${DOT_MAX_SIZE}")
tck_set_test_env(${TEST_NAME} testenv)
unset(testenv)
endfunction(create_testcase)
option(TCK_ENABLE_COMPARE_TESTS "enable tests related to tck_compare" ON)
if(NOT TCK_ENABLE_COMPARE_TESTS)
message(STATUS "tck_compare tests are disabled.")
return()
endif()
# Max number of lines for DOT results
set(DOT_MAX_SIZE 20000)
# Elements of INPUTS are colon-separated lists. The first element of each
# list is a test-case script located in ${EXAMPLES_DIR}; the tail of the list
# contains arguments passed to the generator script.
# only append to the tail of this list!
set(INPUTS
missing_initial.sh:
ad94.sh:
corsso.sh:2:2:10:1:2
critical-region-async.sh:2:10
csmacd.sh:3
dining-philosophers.sh:3:3:10:0
fischer-async.sh:3:10
fischer-async-concurrent.sh:3:10
parallel-c.sh:3
train_gate.sh:2
train_gate.sh:3
)
if(NOT USEINT16)
list(APPEND INPUTS
ad94_mid.sh:)
endif()
if(USEINT64)
list(APPEND INPUTS
ad94_Long.sh:)
endif()
file(RELATIVE_PATH here ${CMAKE_BINARY_DIR} ${CMAKE_CURRENT_BINARY_DIR})
message(STATUS "Generating '${here}' tests. This may take a long time.")
tck_register_testcases("tck-compare-" CHECK_TESTCASES_ savelist TCK_COMPARE_INPUT_FILES ${INPUTS})
# TODO: Insert real Testcases here. You can find the name of all the available files in TCK_COMPARE_INPUT_FILES or add some to INPUTS
list(GET TCK_COMPARE_INPUT_FILES 0 no_initial)
list(GET TCK_COMPARE_INPUT_FILES 1 ad)
create_testcase(no_initial_first ${no_initial} ${ad} strong-timed-bisim)
create_testcase(no_initial_second ${ad} ${no_initial} strong-timed-bisim)
tck_add_savelist(save-compare ${savelist})

1
test/tck-compare/no_initial_first.err-expected Normal file
View file

@ -0,0 +1 @@
WARNING: the first system has no initial state

6
test/tck-compare/no_initial_first.out-expected Normal file
View file

@ -0,0 +1,6 @@
DEEPEST_PATH 0
MEMORY_MAX_RSS xxxx
RELATIONSHIP_FULFILLED true
RUNNING_TIME_SECONDS xxxx
VISITED_PAIR_OF_STATES_STATES 0
VISITED_TRANSITIONS 0

1
test/tck-compare/no_initial_second.err-expected Normal file
View file

@ -0,0 +1 @@
WARNING: the second system has no initial state

6
test/tck-compare/no_initial_second.out-expected Normal file
View file

@ -0,0 +1,6 @@
DEEPEST_PATH 0
MEMORY_MAX_RSS xxxx
RELATIONSHIP_FULFILLED true
RUNNING_TIME_SECONDS xxxx
VISITED_PAIR_OF_STATES_STATES 0
VISITED_TRANSITIONS 0

26
test/tck-compare/tck-compare-ad94.out-expected Normal file
View file

@ -0,0 +1,26 @@
# labels=green
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
system:ad94_fig10
clock:1:x
clock:1:y
event:a
event:b
event:c
event:d
process:P
location:P:l0{initial:}
location:P:l1{}
location:P:l2{}
location:P:l3{labels: green}
edge:P:l0:l1:a{do:y=0}
edge:P:l1:l2:b{provided: y==1}
edge:P:l1:l3:c{provided: x<1}
edge:P:l2:l3:c{provided: x<1}
edge:P:l3:l1:a{provided: y<1 : do:y=0}
edge:P:l3:l3:d{provided: x>1}

26
test/tck-compare/tck-compare-ad94_mid.out-expected Normal file
View file

@ -0,0 +1,26 @@
# labels=green
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
system:ad94_fig10
clock:1:x
clock:1:y
event:a
event:b
event:c
event:d
process:P
location:P:l0{initial:}
location:P:l1{}
location:P:l2{}
location:P:l3{labels: green}
edge:P:l0:l1:a{do:y=0}
edge:P:l1:l2:b{provided: y==100000000}
edge:P:l1:l3:c{provided: x<100000000}
edge:P:l2:l3:c{provided: x<100000000}
edge:P:l3:l1:a{provided: y<100000000 : do:y=0}
edge:P:l3:l3:d{provided: x>100000000}

35
test/tck-compare/tck-compare-corsso_2_2_10_1_2.out-expected Normal file
View file

@ -0,0 +1,35 @@
#labels=access1:access2
system:CorSSO_2_2_10_1_2
event:tau
# Process 1
process:P1
clock:1:x1
clock:1:y1
int:1:0:3:0:a1
int:1:0:3:0:p1
location:P1:auth{initial:}
location:P1:access{labels: access1}
edge:P1:auth:auth:tau{provided: p1>0 && x1>2 && a1<2 : do: a1=a1+1; x1=0}
edge:P1:auth:auth:tau{provided: p1==0 : do: p1=1; a1=0; x1=0; y1=0}
edge:P1:auth:access:tau{provided: y1<10 && p1==1 && a1 >= 1}
edge:P1:auth:auth:tau{provided: p1==0 : do: p1=2; a1=0; x1=0; y1=0}
edge:P1:auth:access:tau{provided: y1<10 && p1==2 && a1 >= 2}
edge:P1:access:auth:tau{do: p1=0}
# Process 2
process:P2
clock:1:x2
clock:1:y2
int:1:0:3:0:a2
int:1:0:3:0:p2
location:P2:auth{initial:}
location:P2:access{labels: access2}
edge:P2:auth:auth:tau{provided: p2>0 && x2>2 && a2<2 : do: a2=a2+1; x2=0}
edge:P2:auth:auth:tau{provided: p2==0 : do: p2=1; a2=0; x2=0; y2=0}
edge:P2:auth:access:tau{provided: y2<10 && p2==1 && a2 >= 1}
edge:P2:auth:auth:tau{provided: p2==0 : do: p2=2; a2=0; x2=0; y2=0}
edge:P2:auth:access:tau{provided: y2<10 && p2==2 && a2 >= 2}
edge:P2:access:auth:tau{do: p2=0}

93
test/tck-compare/tck-compare-critical-region-async_2_10.out-expected Normal file
View file

@ -0,0 +1,93 @@
#labels=error1:error2
system:critical_region_async_2_10
# Events
event:tau
event:enter1
event:exit1
event:enter2
event:exit2
event:id_eq_0
event:id_lt_2
event:id_eq_2
# ID process (shared variable access through synchronized events)
process:ID
int:1:0:2:0:id
location:ID:l{initial:}
edge:ID:l:l:id_eq_0{provided: id==0 : do: id=1}
edge:ID:l:l:id_lt_2{provided: id<2 : do: id=id+1}
edge:ID:l:l:id_eq_2{provided: id==2: do: id=1}
edge:ID:l:l:enter1{provided: id==1 : do: id=0}
edge:ID:l:l:exit1{do: id=1}
edge:ID:l:l:enter2{provided: id==2 : do: id=0}
edge:ID:l:l:exit2{do: id=2}
# Counter
process:counter
location:counter:I{initial:}
location:counter:C{}
edge:counter:I:C:id_eq_0{}
edge:counter:C:C:id_lt_2{}
edge:counter:C:C:id_eq_2{}
# Arbiter 1
process:arbiter1
location:arbiter1:req{initial:}
location:arbiter1:ack{}
edge:arbiter1:req:ack:enter1
edge:arbiter1:ack:req:exit1
# Arbiter 2
process:arbiter2
location:arbiter2:req{initial:}
location:arbiter2:ack{}
edge:arbiter2:req:ack:enter2
edge:arbiter2:ack:req:exit2
# Prod cell 1
process:prodcell1
clock:1:x1
location:prodcell1:not_ready{initial:}
location:prodcell1:testing{invariant: x1<=10}
location:prodcell1:requesting{}
location:prodcell1:critical{invariant: x1<=20}
location:prodcell1:testing2{invariant: x1<=10}
location:prodcell1:safe{labels: safe1}
location:prodcell1:error{labels: error1}
edge:prodcell1:not_ready:testing:tau{provided: x1<=20 : do: x1=0}
edge:prodcell1:testing:not_ready:tau{provided: x1>=10 : do: x1=0}
edge:prodcell1:testing:requesting:tau{provided: x1<=9}
edge:prodcell1:requesting:critical:enter1{do: x1=0}
edge:prodcell1:critical:error:tau{provided: x1>=20}
edge:prodcell1:critical:testing2:exit1{provided: x1<=9 : do: x1=0}
edge:prodcell1:testing2:error:tau{provided: x1>=10}
edge:prodcell1:testing2:safe:tau{provided: x1<=9}
# Prod cell 2
process:prodcell2
clock:1:x2
location:prodcell2:not_ready{initial:}
location:prodcell2:testing{invariant: x2<=10}
location:prodcell2:requesting{}
location:prodcell2:critical{invariant: x2<=20}
location:prodcell2:testing2{invariant: x2<=10}
location:prodcell2:safe{labels: safe2}
location:prodcell2:error{labels: error2}
edge:prodcell2:not_ready:testing:tau{provided: x2<=20 : do: x2=0}
edge:prodcell2:testing:not_ready:tau{provided: x2>=10 : do: x2=0}
edge:prodcell2:testing:requesting:tau{provided: x2<=9}
edge:prodcell2:requesting:critical:enter2{do: x2=0}
edge:prodcell2:critical:error:tau{provided: x2>=20}
edge:prodcell2:critical:testing2:exit2{provided: x2<=9 : do: x2=0}
edge:prodcell2:testing2:error:tau{provided: x2>=10}
edge:prodcell2:testing2:safe:tau{provided: x2<=9}
# Synchronizations
sync:counter@id_eq_0:ID@id_eq_0
sync:counter@id_lt_2:ID@id_lt_2
sync:counter@id_eq_2:ID@id_eq_2
sync:arbiter1@enter1:prodcell1@enter1:ID@enter1
sync:arbiter1@exit1:prodcell1@exit1:ID@exit1
sync:arbiter2@enter2:prodcell2@enter2:ID@enter2
sync:arbiter2@exit2:prodcell2@exit2:ID@exit2

89
test/tck-compare/tck-compare-csmacd_3.out-expected Normal file
View file

@ -0,0 +1,89 @@
system:csmacd_3_808_26
event:tau
event:begin
event:busy
event:end
event:cd
event:cd1
event:cd2
event:cd3
# Bus
process:Bus
int:1:1:4:1:j
clock:1:y
location:Bus:Idle{initial:}
location:Bus:Active{}
location:Bus:Collision{invariant:y<26}
location:Bus:Loop{committed:}
edge:Bus:Idle:Active:begin{do:y=0}
edge:Bus:Active:Collision:begin{provided:y<26 : do:y=0}
edge:Bus:Active:Active:busy{provided:y>=26}
edge:Bus:Active:Idle:end{do:y=0}
edge:Bus:Collision:Loop:tau{provided:y<26 : do:j=1}
edge:Bus:Loop:Idle:tau{provided:j==3+1&&y<26 : do:y=0;j=1}
edge:Bus:Loop:Loop:cd1{provided:j==1 : do:j=j+1}
edge:Bus:Loop:Loop:cd2{provided:j==2 : do:j=j+1}
edge:Bus:Loop:Loop:cd3{provided:j==3 : do:j=j+1}
# Station 1
process:Station1
clock:1:x1
location:Station1:Wait{initial:}
location:Station1:Start{invariant:x1<=808}
location:Station1:Retry{invariant:x1<2*26}
edge:Station1:Wait:Start:begin{do:x1=0}
edge:Station1:Wait:Retry:busy{do:x1=0}
edge:Station1:Wait:Wait:cd{do:x1=0}
edge:Station1:Wait:Retry:cd{do:x1=0}
edge:Station1:Start:Wait:end{provided:x1==808 : do:x1=0}
edge:Station1:Start:Retry:cd{provided:x1<26 : do:x1=0}
edge:Station1:Retry:Start:begin{provided:x1<2*26 : do:x1=0}
edge:Station1:Retry:Retry:busy{provided:x1<2*26 : do:x1=0}
edge:Station1:Retry:Retry:cd{provided:x1<2*26 : do:x1=0}
sync:Bus@begin:Station1@begin
sync:Bus@busy:Station1@busy
sync:Bus@cd1:Station1@cd
sync:Bus@end:Station1@end
# Station 2
process:Station2
clock:1:x2
location:Station2:Wait{initial:}
location:Station2:Start{invariant:x2<=808}
location:Station2:Retry{invariant:x2<2*26}
edge:Station2:Wait:Start:begin{do:x2=0}
edge:Station2:Wait:Retry:busy{do:x2=0}
edge:Station2:Wait:Wait:cd{do:x2=0}
edge:Station2:Wait:Retry:cd{do:x2=0}
edge:Station2:Start:Wait:end{provided:x2==808 : do:x2=0}
edge:Station2:Start:Retry:cd{provided:x2<26 : do:x2=0}
edge:Station2:Retry:Start:begin{provided:x2<2*26 : do:x2=0}
edge:Station2:Retry:Retry:busy{provided:x2<2*26 : do:x2=0}
edge:Station2:Retry:Retry:cd{provided:x2<2*26 : do:x2=0}
sync:Bus@begin:Station2@begin
sync:Bus@busy:Station2@busy
sync:Bus@cd2:Station2@cd
sync:Bus@end:Station2@end
# Station 3
process:Station3
clock:1:x3
location:Station3:Wait{initial:}
location:Station3:Start{invariant:x3<=808}
location:Station3:Retry{invariant:x3<2*26}
edge:Station3:Wait:Start:begin{do:x3=0}
edge:Station3:Wait:Retry:busy{do:x3=0}
edge:Station3:Wait:Wait:cd{do:x3=0}
edge:Station3:Wait:Retry:cd{do:x3=0}
edge:Station3:Start:Wait:end{provided:x3==808 : do:x3=0}
edge:Station3:Start:Retry:cd{provided:x3<26 : do:x3=0}
edge:Station3:Retry:Start:begin{provided:x3<2*26 : do:x3=0}
edge:Station3:Retry:Retry:busy{provided:x3<2*26 : do:x3=0}
edge:Station3:Retry:Retry:cd{provided:x3<2*26 : do:x3=0}
sync:Bus@begin:Station3@begin
sync:Bus@busy:Station3@busy
sync:Bus@cd3:Station3@cd
sync:Bus@end:Station3@end

86
test/tck-compare/tck-compare-dining-philosophers_3_3_10_0.out-expected Normal file
View file

@ -0,0 +1,86 @@
#labels=eating1:eating2:eating3
system:dining_philosophers_3_3_10_0
# events
event:tau
event:take1
event:release1
event:take2
event:release2
event:take3
event:release3
# Philosopher 1
process:P1
clock:1:x1
location:P1:idle{initial:}
location:P1:acq{invariant: x1<=3}
location:P1:eat{invariant: x1<=10 : labels: eating1}
location:P1:rel{invariant: x1<=0}
edge:P1:idle:acq:take3{do: x1=0}
edge:P1:acq:idle:release3{provided: x1>=3}
edge:P1:acq:eat:take1{provided: x1<=3 : do: x1=0}
edge:P1:eat:rel:release1{provided: x1>=10 : do: x1=0}
edge:P1:rel:idle:release3
# Philosopher 2
process:P2
clock:1:x2
location:P2:idle{initial:}
location:P2:acq{invariant: x2<=3}
location:P2:eat{invariant: x2<=10 : labels: eating2}
location:P2:rel{invariant: x2<=0}
edge:P2:idle:acq:take1{do: x2=0}
edge:P2:acq:idle:release1{provided: x2>=3}
edge:P2:acq:eat:take2{provided: x2<=3 : do: x2=0}
edge:P2:eat:rel:release2{provided: x2>=10 : do: x2=0}
edge:P2:rel:idle:release1
# Philosopher 3
process:P3
clock:1:x3
location:P3:idle{initial:}
location:P3:acq{invariant: x3<=3}
location:P3:eat{invariant: x3<=10 : labels: eating3}
location:P3:rel{invariant: x3<=0}
edge:P3:idle:acq:take2{do: x3=0}
edge:P3:acq:idle:release2{provided: x3>=3}
edge:P3:acq:eat:take3{provided: x3<=3 : do: x3=0}
edge:P3:eat:rel:release3{provided: x3>=10 : do: x3=0}
edge:P3:rel:idle:release2
# Fork 1
process:F1
location:F1:free{initial:}
location:F1:taken
edge:F1:free:taken:take1
edge:F1:taken:free:release1
# Fork 2
process:F2
location:F2:free{initial:}
location:F2:taken
edge:F2:free:taken:take2
edge:F2:taken:free:release2
# Fork 3
process:F3
location:F3:free{initial:}
location:F3:taken
edge:F3:free:taken:take3
edge:F3:taken:free:release3
# Synchronizations
sync:P1@take3:F3@take3
sync:P1@take1:F1@take1
sync:P1@release3:F3@release3
sync:P1@release1:F1@release1
sync:P2@take1:F1@take1
sync:P2@take2:F2@take2
sync:P2@release1:F1@release1
sync:P2@release2:F2@release2
sync:P3@take2:F2@take2
sync:P3@take3:F3@take3
sync:P3@release2:F2@release2
sync:P3@release3:F3@release3

117
test/tck-compare/tck-compare-fischer-async-concurrent_3_10.out-expected Normal file
View file

@ -0,0 +1,117 @@
#labels=cs1:cs2:cs3
system:fischer_async_3_10
event:id_is_0
event:id_to_0
event:id_is_1
event:id_to_1
event:id_is_2
event:id_to_2
event:id_is_3
event:id_to_3
event:tau
# Process 1
process:P1
clock:1:x1
location:P1:A{initial:}
location:P1:req{invariant:x1<=10}
location:P1:wait{}
location:P1:cs{labels:cs1}
edge:P1:A:req:id_is_0{do:x1=0}
edge:P1:req:wait:id_to_1{provided:x1<=10 : do:x1=0}
edge:P1:wait:req:id_is_0{do:x1=0}
edge:P1:wait:cs:id_is_1{provided:x1>10}
edge:P1:cs:A:id_to_0{}
# Process 2
process:P2
clock:1:x2
location:P2:A{initial:}
location:P2:req{invariant:x2<=10}
location:P2:wait{}
location:P2:cs{labels:cs2}
edge:P2:A:req:id_is_0{do:x2=0}
edge:P2:req:wait:id_to_2{provided:x2<=10 : do:x2=0}
edge:P2:wait:req:id_is_0{do:x2=0}
edge:P2:wait:cs:id_is_2{provided:x2>10}
edge:P2:cs:A:id_to_0{}
# Process 3
process:P3
clock:1:x3
location:P3:A{initial:}
location:P3:req{invariant:x3<=10}
location:P3:wait{}
location:P3:cs{labels:cs3}
edge:P3:A:req:id_is_0{do:x3=0}
edge:P3:req:wait:id_to_3{provided:x3<=10 : do:x3=0}
edge:P3:wait:req:id_is_0{do:x3=0}
edge:P3:wait:cs:id_is_3{provided:x3>10}
edge:P3:cs:A:id_to_0{}
# ID 1
process:ID1
int:1:0:3:0:id1
location:ID1:l{initial:}
edge:ID1:l:l:id_is_0{provided: id1==0}
edge:ID1:l:l:id_to_0{do: id1=0}
edge:ID1:l:l:id_is_1{provided: id1==1}
edge:ID1:l:l:id_to_1{do: id1=1}
edge:ID1:l:l:id_is_2{provided: id1==2}
edge:ID1:l:l:id_to_2{do: id1=2}
edge:ID1:l:l:id_is_3{provided: id1==3}
edge:ID1:l:l:id_to_3{do: id1=3}
# ID 2
process:ID2
int:1:0:3:0:id2
location:ID2:l{initial:}
edge:ID2:l:l:id_is_0{provided: id2==0}
edge:ID2:l:l:id_to_0{do: id2=0}
edge:ID2:l:l:id_is_1{provided: id2==1}
edge:ID2:l:l:id_to_1{do: id2=1}
edge:ID2:l:l:id_is_2{provided: id2==2}
edge:ID2:l:l:id_to_2{do: id2=2}
edge:ID2:l:l:id_is_3{provided: id2==3}
edge:ID2:l:l:id_to_3{do: id2=3}
# ID 3
process:ID3
int:1:0:3:0:id3
location:ID3:l{initial:}
edge:ID3:l:l:id_is_0{provided: id3==0}
edge:ID3:l:l:id_to_0{do: id3=0}
edge:ID3:l:l:id_is_1{provided: id3==1}
edge:ID3:l:l:id_to_1{do: id3=1}
edge:ID3:l:l:id_is_2{provided: id3==2}
edge:ID3:l:l:id_to_2{do: id3=2}
edge:ID3:l:l:id_is_3{provided: id3==3}
edge:ID3:l:l:id_to_3{do: id3=3}
# Synchronizations
sync:P1@id_is_0:ID1@id_is_0
sync:P1@id_is_1:ID1@id_is_1
sync:P1@id_is_2:ID1@id_is_2
sync:P1@id_is_3:ID1@id_is_3
sync:P2@id_is_0:ID2@id_is_0
sync:P2@id_is_1:ID2@id_is_1
sync:P2@id_is_2:ID2@id_is_2
sync:P2@id_is_3:ID2@id_is_3
sync:P3@id_is_0:ID3@id_is_0
sync:P3@id_is_1:ID3@id_is_1
sync:P3@id_is_2:ID3@id_is_2
sync:P3@id_is_3:ID3@id_is_3
sync:P1@id_to_0:ID1@id_to_0:ID2@id_to_0:ID3@id_to_0
sync:P2@id_to_0:ID1@id_to_0:ID2@id_to_0:ID3@id_to_0
sync:P3@id_to_0:ID1@id_to_0:ID2@id_to_0:ID3@id_to_0
sync:P1@id_to_1:ID1@id_to_1:ID2@id_to_1:ID3@id_to_1
sync:P2@id_to_1:ID1@id_to_1:ID2@id_to_1:ID3@id_to_1
sync:P3@id_to_1:ID1@id_to_1:ID2@id_to_1:ID3@id_to_1
sync:P1@id_to_2:ID1@id_to_2:ID2@id_to_2:ID3@id_to_2
sync:P2@id_to_2:ID1@id_to_2:ID2@id_to_2:ID3@id_to_2
sync:P3@id_to_2:ID1@id_to_2:ID2@id_to_2:ID3@id_to_2
sync:P1@id_to_3:ID1@id_to_3:ID2@id_to_3:ID3@id_to_3
sync:P2@id_to_3:ID1@id_to_3:ID2@id_to_3:ID3@id_to_3
sync:P3@id_to_3:ID1@id_to_3:ID2@id_to_3:ID3@id_to_3

80
test/tck-compare/tck-compare-fischer-async_3_10.out-expected Normal file
View file

@ -0,0 +1,80 @@
#labels=cs1:cs2:cs3
system:fischer_async_3_10
event:id_is_0
event:id_to_0
event:id_is_1
event:id_to_1
event:id_is_2
event:id_to_2
event:id_is_3
event:id_to_3
event:tau
# Process 1
process:P1
clock:1:x1
location:P1:A{initial:}
location:P1:req{invariant:x1<=10}
location:P1:wait{}
location:P1:cs{labels:cs1}
edge:P1:A:req:id_is_0{do:x1=0}
edge:P1:req:wait:id_to_1{provided:x1<=10 : do:x1=0}
edge:P1:wait:req:id_is_0{do:x1=0}
edge:P1:wait:cs:id_is_1{provided:x1>10}
edge:P1:cs:A:id_to_0{}
# Process 2
process:P2
clock:1:x2
location:P2:A{initial:}
location:P2:req{invariant:x2<=10}
location:P2:wait{}
location:P2:cs{labels:cs2}
edge:P2:A:req:id_is_0{do:x2=0}
edge:P2:req:wait:id_to_2{provided:x2<=10 : do:x2=0}
edge:P2:wait:req:id_is_0{do:x2=0}
edge:P2:wait:cs:id_is_2{provided:x2>10}
edge:P2:cs:A:id_to_0{}
# Process 3
process:P3
clock:1:x3
location:P3:A{initial:}
location:P3:req{invariant:x3<=10}
location:P3:wait{}
location:P3:cs{labels:cs3}
edge:P3:A:req:id_is_0{do:x3=0}
edge:P3:req:wait:id_to_3{provided:x3<=10 : do:x3=0}
edge:P3:wait:req:id_is_0{do:x3=0}
edge:P3:wait:cs:id_is_3{provided:x3>10}
edge:P3:cs:A:id_to_0{}
# Process ID
process:ID
int:1:0:3:0:id
location:ID:l{initial:}
edge:ID:l:l:id_is_0{provided: id==0}
edge:ID:l:l:id_to_0{do: id=0}
edge:ID:l:l:id_is_1{provided: id==1}
edge:ID:l:l:id_to_1{do: id=1}
edge:ID:l:l:id_is_2{provided: id==2}
edge:ID:l:l:id_to_2{do: id=2}
edge:ID:l:l:id_is_3{provided: id==3}
edge:ID:l:l:id_to_3{do: id=3}
# Synchronizations
sync:P1@id_is_0:ID@id_is_0
sync:P1@id_to_0:ID@id_to_0
sync:P1@id_is_1:ID@id_is_1
sync:P1@id_to_1:ID@id_to_1
sync:P2@id_is_0:ID@id_is_0
sync:P2@id_to_0:ID@id_to_0
sync:P2@id_is_2:ID@id_is_2
sync:P2@id_to_2:ID@id_to_2
sync:P3@id_is_0:ID@id_is_0
sync:P3@id_to_0:ID@id_to_0
sync:P3@id_is_3:ID@id_is_3
sync:P3@id_to_3:ID@id_to_3

27
test/tck-compare/tck-compare-missing_initial.out-expected Normal file
View file

@ -0,0 +1,27 @@
# labels=green
# Watch Out! This is an example on how NOT to create a model. The initial location is missing
# This file is a part of the TChecker project.
#
# See files AUTHORS and LICENSE for copyright details.
system:missing_initial
clock:1:x
clock:1:y
event:a
event:b
event:c
event:d
process:P
location:P:l0{}
location:P:l1{}
location:P:l2{}
location:P:l3{labels: green}
edge:P:l0:l1:a{do:y=0}
edge:P:l1:l2:b{provided: y==1}
edge:P:l1:l3:c{provided: x<1}
edge:P:l2:l3:c{provided: x<1}
edge:P:l3:l1:a{provided: y<1 : do:y=0}
edge:P:l3:l3:d{provided: x>1}

57
test/tck-compare/tck-compare-parallel-c_3.out-expected Normal file
View file

@ -0,0 +1,57 @@
#labels=access1:access2:access3
system:parallel_bis3
event:tau
event:acquire
event:release
# Process 1
process:P1
clock:1:x1
location:P1:A{initial:}
location:P1:B{}
location:P1:C{invariant:x1<=3 : labels: access1}
edge:P1:A:B:tau{do:x1=0}
edge:P1:B:A:tau{provided:x1>=1}
edge:P1:B:C:acquire{provided:x1<1 : do:x1=0}
edge:P1:C:A:release{provided:x1>=1}
# Process 2
process:P2
clock:1:x2
location:P2:A{initial:}
location:P2:B{}
location:P2:C{invariant:x2<=3 : labels: access2}
edge:P2:A:B:tau{do:x2=0}
edge:P2:B:A:tau{provided:x2>=1}
edge:P2:B:C:acquire{provided:x2<1 : do:x2=0}
edge:P2:C:A:release{provided:x2>=1}
# Process 3
process:P3
clock:1:x3
location:P3:A{initial:}
location:P3:B{}
location:P3:C{invariant:x3<=3 : labels: access3}
edge:P3:A:B:tau{do:x3=0}
edge:P3:B:A:tau{provided:x3>=1}
edge:P3:B:C:acquire{provided:x3<1 : do:x3=0}
edge:P3:C:A:release{provided:x3>=1}
# Process lock
process:lock
clock:1:y
location:lock:U{initial:}
location:lock:L{}
edge:lock:U:L:acquire{provided:y>=1}
edge:lock:L:U:release{do:y=0}
sync:P1@acquire:lock@acquire
sync:P1@release:lock@release
sync:P2@acquire:lock@acquire
sync:P2@release:lock@release
sync:P3@acquire:lock@acquire
sync:P3@release:lock@release

74
test/tck-compare/tck-compare-train_gate_2.out-expected Normal file
View file

@ -0,0 +1,74 @@
#labels=cross1:cross2
system:train_gate_2
event:tau
event:go
event:appr
event:leave
event:stop
event:go1
event:appr1
event:leave1
event:stop1
event:go2
event:appr2
event:leave2
event:stop2
# Gate
process:Gate
int:2:1:2:1:buffer
int:1:0:1:0:head
int:1:0:2:0:length
location:Gate:Free{initial:}
location:Gate:Occ{}
location:Gate:Transient{committed:}
edge:Gate:Free:Occ:go1{provided:length>0&&buffer[head]==1}
edge:Gate:Free:Occ:appr1{provided:length==0 : do:buffer[(head+length)%2]=1;length=length+1}
edge:Gate:Occ:Transient:appr1{do:buffer[(head+length)%2]=1;length=length+1}
edge:Gate:Occ:Free:leave1{provided:length>0&&buffer[head]==1 : do:head=(head+1)%2;length=length-1}
edge:Gate:Transient:Occ:stop1{provided:length>0&&buffer[(head+length-1)%2]==1}
edge:Gate:Free:Occ:go2{provided:length>0&&buffer[head]==2}
edge:Gate:Free:Occ:appr2{provided:length==0 : do:buffer[(head+length)%2]=2;length=length+1}
edge:Gate:Occ:Transient:appr2{do:buffer[(head+length)%2]=2;length=length+1}
edge:Gate:Occ:Free:leave2{provided:length>0&&buffer[head]==2 : do:head=(head+1)%2;length=length-1}
edge:Gate:Transient:Occ:stop2{provided:length>0&&buffer[(head+length-1)%2]==2}
# Train 1
process:Train1
clock:1:x1
location:Train1:Safe{initial:}
location:Train1:Appr{invariant:x1<=20}
location:Train1:Stop{}
location:Train1:Start{invariant:x1<=15}
location:Train1:Cross{invariant:x1<=5 : labels:cross1}
edge:Train1:Safe:Appr:appr{do:x1=0}
edge:Train1:Appr:Cross:tau{provided:x1>=10 : do:x1=0}
edge:Train1:Appr:Stop:stop{provided:x1<=10}
edge:Train1:Stop:Start:go{do:x1=0}
edge:Train1:Start:Cross:tau{provided:x1>=7 : do:x1=0}
edge:Train1:Cross:Safe:leave{provided:x1>=3}
sync:Train1@appr:Gate@appr1
sync:Train1@stop:Gate@stop1
sync:Train1@go:Gate@go1
sync:Train1@leave:Gate@leave1
# Train 2
process:Train2
clock:1:x2
location:Train2:Safe{initial:}
location:Train2:Appr{invariant:x2<=20}
location:Train2:Stop{}
location:Train2:Start{invariant:x2<=15}
location:Train2:Cross{invariant:x2<=5 : labels:cross2}
edge:Train2:Safe:Appr:appr{do:x2=0}
edge:Train2:Appr:Cross:tau{provided:x2>=10 : do:x2=0}
edge:Train2:Appr:Stop:stop{provided:x2<=10}
edge:Train2:Stop:Start:go{do:x2=0}
edge:Train2:Start:Cross:tau{provided:x2>=7 : do:x2=0}
edge:Train2:Cross:Safe:leave{provided:x2>=3}
sync:Train2@appr:Gate@appr2
sync:Train2@stop:Gate@stop2
sync:Train2@go:Gate@go2
sync:Train2@leave:Gate@leave2

102
test/tck-compare/tck-compare-train_gate_3.out-expected Normal file
View file

@ -0,0 +1,102 @@
#labels=cross1:cross2:cross3
system:train_gate_3
event:tau
event:go
event:appr
event:leave
event:stop
event:go1
event:appr1
event:leave1
event:stop1
event:go2
event:appr2
event:leave2
event:stop2
event:go3
event:appr3
event:leave3
event:stop3
# Gate
process:Gate
int:3:1:3:1:buffer
int:1:0:2:0:head
int:1:0:3:0:length
location:Gate:Free{initial:}
location:Gate:Occ{}
location:Gate:Transient{committed:}
edge:Gate:Free:Occ:go1{provided:length>0&&buffer[head]==1}
edge:Gate:Free:Occ:appr1{provided:length==0 : do:buffer[(head+length)%3]=1;length=length+1}
edge:Gate:Occ:Transient:appr1{do:buffer[(head+length)%3]=1;length=length+1}
edge:Gate:Occ:Free:leave1{provided:length>0&&buffer[head]==1 : do:head=(head+1)%3;length=length-1}
edge:Gate:Transient:Occ:stop1{provided:length>0&&buffer[(head+length-1)%3]==1}
edge:Gate:Free:Occ:go2{provided:length>0&&buffer[head]==2}
edge:Gate:Free:Occ:appr2{provided:length==0 : do:buffer[(head+length)%3]=2;length=length+1}
edge:Gate:Occ:Transient:appr2{do:buffer[(head+length)%3]=2;length=length+1}
edge:Gate:Occ:Free:leave2{provided:length>0&&buffer[head]==2 : do:head=(head+1)%3;length=length-1}
edge:Gate:Transient:Occ:stop2{provided:length>0&&buffer[(head+length-1)%3]==2}
edge:Gate:Free:Occ:go3{provided:length>0&&buffer[head]==3}
edge:Gate:Free:Occ:appr3{provided:length==0 : do:buffer[(head+length)%3]=3;length=length+1}
edge:Gate:Occ:Transient:appr3{do:buffer[(head+length)%3]=3;length=length+1}
edge:Gate:Occ:Free:leave3{provided:length>0&&buffer[head]==3 : do:head=(head+1)%3;length=length-1}
edge:Gate:Transient:Occ:stop3{provided:length>0&&buffer[(head+length-1)%3]==3}
# Train 1
process:Train1
clock:1:x1
location:Train1:Safe{initial:}
location:Train1:Appr{invariant:x1<=20}
location:Train1:Stop{}
location:Train1:Start{invariant:x1<=15}
location:Train1:Cross{invariant:x1<=5 : labels:cross1}
edge:Train1:Safe:Appr:appr{do:x1=0}
edge:Train1:Appr:Cross:tau{provided:x1>=10 : do:x1=0}
edge:Train1:Appr:Stop:stop{provided:x1<=10}
edge:Train1:Stop:Start:go{do:x1=0}
edge:Train1:Start:Cross:tau{provided:x1>=7 : do:x1=0}
edge:Train1:Cross:Safe:leave{provided:x1>=3}
sync:Train1@appr:Gate@appr1
sync:Train1@stop:Gate@stop1
sync:Train1@go:Gate@go1
sync:Train1@leave:Gate@leave1
# Train 2
process:Train2
clock:1:x2
location:Train2:Safe{initial:}
location:Train2:Appr{invariant:x2<=20}
location:Train2:Stop{}
location:Train2:Start{invariant:x2<=15}
location:Train2:Cross{invariant:x2<=5 : labels:cross2}
edge:Train2:Safe:Appr:appr{do:x2=0}
edge:Train2:Appr:Cross:tau{provided:x2>=10 : do:x2=0}
edge:Train2:Appr:Stop:stop{provided:x2<=10}
edge:Train2:Stop:Start:go{do:x2=0}
edge:Train2:Start:Cross:tau{provided:x2>=7 : do:x2=0}
edge:Train2:Cross:Safe:leave{provided:x2>=3}
sync:Train2@appr:Gate@appr2
sync:Train2@stop:Gate@stop2
sync:Train2@go:Gate@go2
sync:Train2@leave:Gate@leave2
# Train 3
process:Train3
clock:1:x3
location:Train3:Safe{initial:}
location:Train3:Appr{invariant:x3<=20}
location:Train3:Stop{}
location:Train3:Start{invariant:x3<=15}
location:Train3:Cross{invariant:x3<=5 : labels:cross3}
edge:Train3:Safe:Appr:appr{do:x3=0}
edge:Train3:Appr:Cross:tau{provided:x3>=10 : do:x3=0}
edge:Train3:Appr:Stop:stop{provided:x3<=10}
edge:Train3:Stop:Start:go{do:x3=0}
edge:Train3:Start:Cross:tau{provided:x3>=7 : do:x3=0}
edge:Train3:Cross:Safe:leave{provided:x3>=3}
sync:Train3@appr:Gate@appr3
sync:Train3@stop:Gate@stop3
sync:Train3@go:Gate@go3
sync:Train3@leave:Gate@leave3