libutap  0.93
Uppaal Timed Automata Parser
Functions
typechecker.cpp File Reference
#include "utap/utap.h"
#include "utap/typechecker.h"
#include "utap/systembuilder.h"
#include <sstream>
#include <list>
#include <stdexcept>
#include <cmath>
#include <cstdio>
#include <cassert>
#include <boost/tuple/tuple.hpp>
Include dependency graph for typechecker.cpp:

Go to the source code of this file.

Functions

static bool isCost (expression_t expr)
 
static bool isVoid (expression_t expr)
 
static bool isDouble (expression_t expr)
 
static bool isInteger (expression_t expr)
 
static bool isBound (expression_t expr)
 
static bool isIntegral (expression_t expr)
 
static bool isClock (expression_t expr)
 
static bool isDiff (expression_t expr)
 
static bool isDoubleValue (expression_t expr)
 
static bool isNumber (expression_t expr)
 
static bool isConstantInteger (expression_t expr)
 
static bool isConstantDouble (expression_t expr)
 
static bool isInvariant (expression_t expr)
 
static bool isGuard (expression_t expr)
 
static bool isConstraint (expression_t expr)
 
static bool isFormula (expression_t expr)
 
static bool isListOfFormulas (expression_t expr)
 
static bool hasStrictLowerBound (expression_t expr)
 
static bool hasStrictUpperBound (expression_t expr)
 
static bool isInvariantWR (expression_t expr)
 Returns true iff type is a valid invariant. More...
 
static bool isAssignable (type_t type)
 Returns true if values of this type can be assigned. More...
 
static bool isGameProperty (expression_t expr)
 
static bool hasMITLInQuantifiedSub (expression_t expr)
 
static bool hasSpawnOrExit (expression_t expr)
 
static bool validReturnType (type_t type)
 
static int channelCapability (type_t type)
 Returns a value indicating the capabilities of a channel. More...
 
static bool isSameScalarType (type_t t1, type_t t2)
 Returns true if two scalar types are name-equivalent. More...
 
static bool isProcessID (expression_t expr)
 
static bool checkIDList (expression_t expr, kind_t kind)
 
bool parseXTA (FILE *file, TimedAutomataSystem *system, bool newxta)
 
bool parseXTA (const char *buffer, TimedAutomataSystem *system, bool newxta)
 
int32_t parseXMLBuffer (const char *buffer, TimedAutomataSystem *system, bool newxta)
 
int32_t parseXMLFile (const char *file, TimedAutomataSystem *system, bool newxta)
 
expression_t parseExpression (const char *str, TimedAutomataSystem *system, bool newxtr)
 

Function Documentation

◆ channelCapability()

static int channelCapability ( type_t  type)
static

Returns a value indicating the capabilities of a channel.

For urgent channels this is 0, for non-urgent broadcast channels this is 1, and in all other cases 2. An argument to a channel parameter must have at least the same capability as the parameter.

Definition at line 1761 of file typechecker.cpp.

References UTAP::Constants::BROADCAST, UTAP::type_t::is(), UTAP::type_t::isChannel(), and UTAP::Constants::URGENT.

Referenced by isSameScalarType().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ checkIDList()

static bool checkIDList ( expression_t  expr,
kind_t  kind 
)
static

Definition at line 2080 of file typechecker.cpp.

References UTAP::expression_t::getKind(), UTAP::expression_t::getSize(), isProcessID(), and UTAP::Constants::LIST.

Referenced by UTAP::TypeChecker::checkExpression().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ hasMITLInQuantifiedSub()

static bool hasMITLInQuantifiedSub ( expression_t  expr)
static

Definition at line 1335 of file typechecker.cpp.

References UTAP::expression_t::get(), UTAP::expression_t::getKind(), UTAP::expression_t::getSize(), UTAP::Constants::MITLEXISTS, and UTAP::Constants::MITLFORALL.

Referenced by UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ hasSpawnOrExit()

static bool hasSpawnOrExit ( expression_t  expr)
static

Definition at line 1348 of file typechecker.cpp.

References UTAP::Constants::EXIT, UTAP::expression_t::get(), UTAP::expression_t::getKind(), UTAP::expression_t::getSize(), and UTAP::Constants::SPAWN.

Here is the call graph for this function:

◆ hasStrictLowerBound()

static bool hasStrictLowerBound ( expression_t  expr)
static

Definition at line 162 of file typechecker.cpp.

References UTAP::expression_t::getKind(), UTAP::expression_t::getSize(), UTAP::Constants::GT, isClock(), isIntegral(), and UTAP::Constants::LT.

Referenced by UTAP::TypeChecker::visitEdge().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ hasStrictUpperBound()

static bool hasStrictUpperBound ( expression_t  expr)
static

Definition at line 193 of file typechecker.cpp.

References UTAP::expression_t::getKind(), UTAP::expression_t::getSize(), UTAP::Constants::GT, isClock(), isIntegral(), and UTAP::Constants::LT.

Referenced by UTAP::TypeChecker::visitEdge().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isAssignable()

static bool isAssignable ( type_t  type)
static

Returns true if values of this type can be assigned.

This is the case for integers, booleans, clocks, cost, scalars and arrays and records of these. E.g. channels and processes are not assignable.

Definition at line 238 of file typechecker.cpp.

References UTAP::Constants::ARRAY, UTAP::Constants::BOOL, UTAP::Constants::CLOCK, UTAP::Constants::COST, UTAP::Constants::DOUBLE, UTAP::type_t::getKind(), UTAP::Constants::INT, UTAP::Constants::RECORD, UTAP::Constants::SCALAR, and UTAP::type_t::size().

Referenced by UTAP::TypeChecker::checkExpression(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isBound()

static bool isBound ( expression_t  expr)
static

Definition at line 77 of file typechecker.cpp.

References UTAP::expression_t::getType(), UTAP::type_t::isDouble(), and UTAP::type_t::isInteger().

Referenced by UTAP::TypeChecker::checkExpression().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isClock()

static bool isClock ( expression_t  expr)
static

Definition at line 87 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isClock().

Referenced by UTAP::TypeChecker::checkDynamicExpressions(), UTAP::TypeChecker::checkExpression(), hasStrictLowerBound(), hasStrictUpperBound(), isDoubleValue(), UTAP::expression_t::usesClock(), UTAP::TypeChecker::visitHybridClock(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isConstantDouble()

static bool isConstantDouble ( expression_t  expr)
static

Definition at line 112 of file typechecker.cpp.

References UTAP::Constants::CONSTANT, UTAP::expression_t::getKind(), and isDouble().

Referenced by UTAP::TypeChecker::checkDynamicExpressions().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isConstantInteger()

static bool isConstantInteger ( expression_t  expr)
static

Definition at line 107 of file typechecker.cpp.

References UTAP::Constants::CONSTANT, UTAP::expression_t::getKind(), and isInteger().

Referenced by UTAP::TypeChecker::checkDynamicExpressions().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isConstraint()

static bool isConstraint ( expression_t  expr)
static

Definition at line 134 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isConstraint().

Referenced by UTAP::TypeChecker::checkDynamicExpressions(), UTAP::TypeChecker::checkExpression(), UTAP::type_t::isFormula(), UTAP::TypeChecker::visitGanttChart(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isCost()

static bool isCost ( expression_t  expr)
static

Definition at line 52 of file typechecker.cpp.

References UTAP::Constants::COST, UTAP::expression_t::getType(), and UTAP::type_t::is().

Referenced by UTAP::TypeChecker::checkExpression(), and UTAP::CompileTimeComputableValues::contains().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isDiff()

static bool isDiff ( expression_t  expr)
static

Definition at line 92 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isDiff().

Referenced by UTAP::TypeChecker::checkExpression(), isDoubleValue(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isDouble()

static bool isDouble ( expression_t  expr)
static

Definition at line 62 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isDouble().

Referenced by isConstantDouble(), and isDoubleValue().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isDoubleValue()

static bool isDoubleValue ( expression_t  expr)
static

Definition at line 97 of file typechecker.cpp.

References isClock(), isDiff(), and isDouble().

Referenced by UTAP::TypeChecker::checkDynamicExpressions(), UTAP::TypeChecker::checkExpression(), and isNumber().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isFormula()

static bool isFormula ( expression_t  expr)
static

Definition at line 139 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isFormula().

Referenced by UTAP::TypeChecker::checkExpression(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isGameProperty()

static bool isGameProperty ( expression_t  expr)
static

Definition at line 1310 of file typechecker.cpp.

References UTAP::Constants::CONSISTENCY, UTAP::Constants::CONTROL, UTAP::Constants::CONTROL_TOPT, UTAP::Constants::CONTROL_TOPT_DEF1, UTAP::Constants::CONTROL_TOPT_DEF2, UTAP::Constants::EF_CONTROL, UTAP::expression_t::getKind(), UTAP::Constants::IMPLEMENTATION, UTAP::Constants::PO_CONTROL, UTAP::Constants::REFINEMENT_GE, UTAP::Constants::REFINEMENT_LE, UTAP::Constants::SIMULATION_GE, UTAP::Constants::SIMULATION_LE, UTAP::Constants::SMC_CONTROL, and UTAP::Constants::SPECIFICATION.

Referenced by UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isGuard()

static bool isGuard ( expression_t  expr)
static

Definition at line 122 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isGuard().

Referenced by UTAP::TypeChecker::checkExpression(), UTAP::type_t::isConstraint(), UTAP::TypeChecker::visitCondition(), and UTAP::TypeChecker::visitEdge().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isInteger()

static bool isInteger ( expression_t  expr)
static

Definition at line 72 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isInteger().

Referenced by UTAP::TypeChecker::checkExpression(), isConstantInteger(), UTAP::type_t::isGuard(), UTAP::TypeChecker::TypeChecker(), UTAP::TypeChecker::visitIODecl(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isIntegral()

static bool isIntegral ( expression_t  expr)
static

Definition at line 82 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isIntegral().

Referenced by UTAP::TypeChecker::checkDynamicExpressions(), UTAP::TypeChecker::checkExpression(), hasStrictLowerBound(), hasStrictUpperBound(), UTAP::type_t::isInvariant(), isNumber(), UTAP::TypeChecker::visitEdge(), UTAP::TypeChecker::visitGanttChart(), UTAP::TypeChecker::visitProgressMeasure(), UTAP::TypeChecker::visitProperty(), and UTAP::TypeChecker::visitState().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isInvariant()

static bool isInvariant ( expression_t  expr)
static

Definition at line 117 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isInvariant().

Referenced by UTAP::TypeChecker::checkExpression(), UTAP::CompileTimeComputableValues::contains(), UTAP::type_t::isGuard(), and isInvariantWR().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isInvariantWR()

static bool isInvariantWR ( expression_t  expr)
static

Returns true iff type is a valid invariant.

A valid invariant is either an invariant expression or an integer expression.

Definition at line 228 of file typechecker.cpp.

References UTAP::expression_t::getType(), UTAP::Constants::INVARIANT_WR, UTAP::type_t::is(), and isInvariant().

Referenced by UTAP::TypeChecker::checkExpression(), UTAP::CompileTimeComputableValues::contains(), and UTAP::TypeChecker::visitState().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isListOfFormulas()

static bool isListOfFormulas ( expression_t  expr)
static

Definition at line 144 of file typechecker.cpp.

References UTAP::expression_t::getKind(), UTAP::expression_t::getSize(), and UTAP::Constants::LIST.

Referenced by UTAP::TypeChecker::checkExpression().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isNumber()

static bool isNumber ( expression_t  expr)
static

Definition at line 102 of file typechecker.cpp.

References isDoubleValue(), and isIntegral().

Referenced by UTAP::TypeChecker::checkExpression().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isProcessID()

static bool isProcessID ( expression_t  expr)
static

Definition at line 2075 of file typechecker.cpp.

References UTAP::expression_t::getKind(), UTAP::expression_t::getType(), UTAP::Constants::IDENTIFIER, UTAP::type_t::is(), and UTAP::Constants::PROCESS.

Referenced by UTAP::TypeChecker::checkExpression(), and checkIDList().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isSameScalarType()

static bool isSameScalarType ( type_t  t1,
type_t  t2 
)
static

Returns true if two scalar types are name-equivalent.

Definition at line 1778 of file typechecker.cpp.

References channelCapability(), UTAP::Constants::CONSTANT, UTAP::expression_t::createNary(), UTAP::Constants::EF, UTAP::type_t::findIndexOf(), UTAP::type_t::getArraySize(), UTAP::expression_t::getKind(), UTAP::type_t::getKind(), UTAP::type_t::getLabel(), UTAP::expression_t::getPosition(), UTAP::type_t::getRange(), UTAP::type_t::getRecordLabel(), UTAP::type_t::getRecordSize(), UTAP::expression_t::getSize(), UTAP::type_t::getSub(), UTAP::expression_t::getType(), UTAP::type_t::is(), UTAP::type_t::isArray(), UTAP::type_t::isBoolean(), UTAP::type_t::isChannel(), UTAP::type_t::isClock(), UTAP::type_t::isConstant(), UTAP::type_t::isDouble(), UTAP::type_t::isInteger(), UTAP::type_t::isIntegral(), UTAP::type_t::isRecord(), UTAP::type_t::isScalar(), UTAP::Constants::LABEL, UTAP::Constants::LIST, UTAP::Constants::PROCESSVAR, UTAP::Constants::RANGE, UTAP::Constants::REF, UTAP::Constants::SCALAR, UTAP::type_t::size(), and UTAP::Constants::SYSTEM_META.

Referenced by UTAP::TypeChecker::checkExpression().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isVoid()

static bool isVoid ( expression_t  expr)
static

Definition at line 57 of file typechecker.cpp.

References UTAP::expression_t::getType(), and UTAP::type_t::isVoid().

Referenced by UTAP::TypeChecker::checkExpression(), and UTAP::TypeChecker::visitProperty().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ parseExpression()

expression_t parseExpression ( const char *  str,
TimedAutomataSystem *  system,
bool  newxtr 
)

Definition at line 3377 of file typechecker.cpp.

References UTAP::TypeChecker::checkExpression(), UTAP::ExpressionBuilder::getExpressions(), UTAP::TimedAutomataSystem::hasErrors(), parseXTA(), and UTAP::S_EXPRESSION.

Here is the call graph for this function:

◆ parseXMLBuffer()

int32_t parseXMLBuffer ( const char *  buffer,
TimedAutomataSystem *  system,
bool  newxta 
)

Definition at line 3336 of file typechecker.cpp.

References UTAP::TimedAutomataSystem::accept(), UTAP::TimedAutomataSystem::hasErrors(), and parseXMLBuffer().

Referenced by parseXMLBuffer().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ parseXMLFile()

int32_t parseXMLFile ( const char *  file,
TimedAutomataSystem *  system,
bool  newxta 
)

Definition at line 3357 of file typechecker.cpp.

References UTAP::TimedAutomataSystem::accept(), UTAP::TimedAutomataSystem::hasErrors(), and parseXMLFile().

Referenced by main(), and parseXMLFile().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ parseXTA() [1/2]

bool parseXTA ( FILE *  file,
TimedAutomataSystem *  system,
bool  newxta 
)

Definition at line 3312 of file typechecker.cpp.

References UTAP::TimedAutomataSystem::accept(), UTAP::TimedAutomataSystem::hasErrors(), and parseXTA().

Referenced by parseExpression(), and parseXTA().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ parseXTA() [2/2]

bool parseXTA ( const char *  buffer,
TimedAutomataSystem *  system,
bool  newxta 
)

Definition at line 3324 of file typechecker.cpp.

References UTAP::TimedAutomataSystem::accept(), UTAP::TimedAutomataSystem::hasErrors(), and parseXTA().

Here is the call graph for this function:

◆ validReturnType()

static bool validReturnType ( type_t  type)
static

Definition at line 1535 of file typechecker.cpp.

References UTAP::Constants::BOOL, UTAP::Constants::DOUBLE, UTAP::type_t::getKind(), UTAP::Constants::INT, UTAP::Constants::LABEL, UTAP::Constants::RANGE, UTAP::Constants::RECORD, UTAP::Constants::SCALAR, and UTAP::type_t::size().

Referenced by UTAP::TypeChecker::visitFunction().

Here is the call graph for this function:
Here is the caller graph for this function: