You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
594 lines
16 KiB
594 lines
16 KiB
//==============================================================================
|
|
//
|
|
// Copyright (c) 2004-2005, Andrew Hinton
|
|
//
|
|
// This file is part of PRISM.
|
|
//
|
|
// PRISM is free software; you can redistribute it and/or modify
|
|
// it under the terms of the GNU General Public License as published by
|
|
// the Free Software Foundation; either version 2 of the License, or
|
|
// (at your option) any later version.
|
|
//
|
|
// PRISM is distributed in the hope that it will be useful,
|
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
// GNU General Public License for more details.
|
|
//
|
|
// You should have received a copy of the GNU General Public License
|
|
// along with PRISM; if not, write to the Free Software Foundation,
|
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|
|
//
|
|
//==============================================================================
|
|
|
|
#ifndef _Included_simulator_Pctlheader
|
|
#define _Included_simulator_Pctlheader
|
|
|
|
#include "simexpression.h"
|
|
#include "simstate.h"
|
|
#include "simupdater.h"
|
|
#include <string>
|
|
#include <iostream>
|
|
|
|
using std::string;
|
|
using std::cout;
|
|
using std::endl;
|
|
|
|
|
|
//=============================================================================
|
|
// Description
|
|
//=============================================================================
|
|
|
|
/*
|
|
* This interface provides the means of reasoning about executions through
|
|
* models. It stores a collection of CPathFormula or CRewardFormula objects.
|
|
* These objects should be notified about any updates in the state, so that
|
|
* they can reason about the path as a whole. These updates should be notified
|
|
* in order and each object can be reset to look at a new path.
|
|
*/
|
|
|
|
//=============================================================================
|
|
// Constants
|
|
//=============================================================================
|
|
|
|
const int FORMULA_BOUNDED_UNTIL = 0;
|
|
const int FORMULA_UNTIL = 1;
|
|
const int FORMULA_NEXT = 2;
|
|
const int FORMULA_CUMULATIVE = 3;
|
|
const int FORMULA_REACHABILITY = 4;
|
|
const int FORMULA_INSTANTANEOUS = 5;
|
|
|
|
|
|
//=============================================================================
|
|
//Class definitions
|
|
//=============================================================================
|
|
|
|
/*
|
|
* CPathFormula
|
|
* ===========
|
|
*
|
|
* The CPathFormula class is used to represent any form of reasoning about
|
|
* paths. Primarily, this is used for (bounded/unbounded) untils and
|
|
* next operators, but is also overridden for specific support for rewards
|
|
* based operators.
|
|
*
|
|
* The important method is the Notify_State() method which should be overridden
|
|
* by each type of path operator to deal with an addition to the execution
|
|
* path. When the answer for a particular path is known, answer_known is
|
|
* set to true and the result is stored in answer. At this point no more
|
|
* evaluation of the path property is necessary.
|
|
*/
|
|
class CPathFormula
|
|
{
|
|
protected:
|
|
bool answer;
|
|
|
|
public:
|
|
bool answer_known;
|
|
/*
|
|
* Constructor for CPathFormula object.
|
|
*/
|
|
CPathFormula();
|
|
|
|
/*
|
|
* Virtual destructor for a CPathFormula object.
|
|
*/
|
|
virtual ~CPathFormula()
|
|
{
|
|
}
|
|
|
|
/*
|
|
* Access to the calculated answer for this CPathFormula object.
|
|
*/
|
|
bool Get_Answer();
|
|
|
|
/*
|
|
* Access to a real number version of the answer for this CPathFormula
|
|
* object.
|
|
*/
|
|
virtual double Get_Answer_Double();
|
|
|
|
/*
|
|
* Resets this CPathFormula object for use in future calcuations.
|
|
*/
|
|
virtual void Reset();
|
|
|
|
/*
|
|
* This method should be overridden by all reward subclasses to return
|
|
* true.
|
|
*/
|
|
virtual bool Is_Reward();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method should be overridden to determine whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
virtual void Notify_State(CPathState* last_state, int* current_state)=0;
|
|
|
|
/*
|
|
* This method should be overridden to give a string representation of the
|
|
* path or reward formula.
|
|
*/
|
|
virtual string To_String() =0;
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula.
|
|
*/
|
|
virtual bool Is_Answer_Known(CLoopDetectionHandler* loop_detection)=0;
|
|
|
|
virtual void Write_Formula(int fd)=0;
|
|
|
|
};
|
|
|
|
/*
|
|
* CRewardFormula
|
|
* ==============
|
|
*
|
|
* The CRewardFormula class overrides CPathFormula to provide specific
|
|
* support for reward operators. Essentially it provides an extra
|
|
* variables answer_double which is used to store the calculated reward
|
|
* for an execution path. This can be queried by Get_Answer_Double().
|
|
*
|
|
*/
|
|
class CRewardFormula : public CPathFormula
|
|
{
|
|
|
|
protected:
|
|
double answer_double; //used to store the reward answer
|
|
int reward_struct_index; //used to store the reward strcuture index
|
|
|
|
public:
|
|
/*
|
|
* Constructor for a CRewardFormula object.
|
|
*/
|
|
CRewardFormula();
|
|
|
|
/*
|
|
* Returns the calculated reward for this CRewardFormula.
|
|
*/
|
|
double Get_Answer_Double();
|
|
|
|
/*
|
|
* Returns the reward structure index for this CRewardFormula.
|
|
*/
|
|
int Get_Reward_Struct_Index();
|
|
|
|
/*
|
|
* Resets this CRewardFormula object for use in future calcuations.
|
|
*/
|
|
virtual void Reset();
|
|
|
|
/*
|
|
* Overridden to state that this object should be treated as a reward
|
|
* formulae.
|
|
*/
|
|
bool Is_Reward();
|
|
|
|
virtual void Write_Formula(int fd)=0;
|
|
};
|
|
|
|
/*
|
|
* CBoundedUntil
|
|
* ==============
|
|
*
|
|
* The CBoundedUntil class is used to store and deal with path formulae of the form:
|
|
* [ leftExpression U[lower_bound, upper_bound] rightExpression ].
|
|
* i.e. leftExpression must hold true until rightExpression is satisfied within
|
|
* the lower and upper time bounds. For CTMCs, the time bounds refer to real time
|
|
* but for DTMCs, this bound refers to time steps.
|
|
*
|
|
*/
|
|
class CBoundedUntil : public CPathFormula
|
|
{
|
|
private:
|
|
CExpression* leftExpression;
|
|
CExpression* rightExpression;
|
|
double upper_bound;
|
|
double lower_bound;
|
|
int counter;
|
|
double time_so_far;
|
|
|
|
public:
|
|
|
|
/*
|
|
* Constructor for a CBoundedUntil object.
|
|
*/
|
|
CBoundedUntil(CExpression* leftExpression, CExpression* rightExpression, double lower_bound, double bound);
|
|
|
|
/*
|
|
* Destructor for a CBoundedUntil object. Deletes the left and right expression
|
|
* structures.
|
|
*/
|
|
~CBoundedUntil();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method determines whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
void Notify_State(CPathState* last_state, int* current_state);
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula. This
|
|
* will either be if the answer has been proven, or if the answer has not been
|
|
* determined but the path is looping.
|
|
*/
|
|
bool Is_Answer_Known(CLoopDetectionHandler* loop_detection);
|
|
|
|
/*
|
|
* Returns a string representation of this CBoundedUntil object.
|
|
*/
|
|
string To_String();
|
|
|
|
/*
|
|
* Resets the counter and time_so_far variables, and calls the superclass Reset method.
|
|
*/
|
|
void Reset();
|
|
|
|
void Write_Formula(int fd);
|
|
};
|
|
|
|
/*
|
|
* CUntil
|
|
* ======
|
|
*
|
|
* The CUntil class is used to store and deal with path formulae of the form:
|
|
* [ leftExpression U rightExpression ].
|
|
* i.e. leftExpression must hold true until rightExpression is satisfied.
|
|
*
|
|
*/
|
|
class CUntil : public CPathFormula
|
|
{
|
|
private:
|
|
CExpression* leftExpression;
|
|
CExpression* rightExpression;
|
|
|
|
public:
|
|
|
|
/*
|
|
* Constructor for a CUntil object.
|
|
*/
|
|
CUntil(CExpression* leftExpression, CExpression* rightExpression);
|
|
|
|
/*
|
|
* Destructor for a CBoundedUntil object. Deletes the left and right expression
|
|
* structures.
|
|
*/
|
|
~CUntil();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method determines whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
void Notify_State(CPathState* last_state, int* current_state);
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula. This
|
|
* will either be if the answer has been proven, or if the answer has not been
|
|
* determined but the path is looping.
|
|
*/
|
|
bool Is_Answer_Known(CLoopDetectionHandler* loop_detection);
|
|
|
|
/*
|
|
* Returns a string representation of this CUntil object.
|
|
*/
|
|
string To_String();
|
|
|
|
void Write_Formula(int fd);
|
|
};
|
|
|
|
/*
|
|
* CNext
|
|
* =====
|
|
*
|
|
* The CNext class is used to store and deal with path formulae of the form:
|
|
* [ X expression ].
|
|
* i.e. expression must hold true in the state following the original state.
|
|
*
|
|
*/
|
|
class CNext : public CPathFormula
|
|
{
|
|
private:
|
|
CExpression* expression;
|
|
int counter;
|
|
|
|
public:
|
|
|
|
/*
|
|
* Constructor for a CNext object.
|
|
*/
|
|
CNext(CExpression* expression);
|
|
|
|
/*
|
|
* Destructor for a CNextUntil object. Deletes the expression
|
|
* structure.
|
|
*/
|
|
~CNext();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method determines whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
void Notify_State(CPathState* last_state, int* current_state);
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula. This
|
|
* will either be if the answer has been proven, or if the answer has not been
|
|
* determined but the path is looping.
|
|
*/
|
|
bool Is_Answer_Known(CLoopDetectionHandler* loop_detection);
|
|
|
|
/*
|
|
* Returns a string representation of this CNext object.
|
|
*/
|
|
string To_String();
|
|
|
|
/*
|
|
* Resets the counter for this CNext object and calls the superclass Reset method.
|
|
*/
|
|
void Reset();
|
|
|
|
void Write_Formula(int fd);
|
|
};
|
|
|
|
/*
|
|
* CRewardCumulative
|
|
* =================
|
|
*
|
|
* The CRewardCumulative class is used to store and deal with rewards formulae
|
|
* of the form:
|
|
* [ C<=time ].
|
|
* i.e. What is the reward accumulated before the time bound
|
|
*
|
|
*/
|
|
class CRewardCumulative : public CRewardFormula
|
|
{
|
|
private:
|
|
double time;
|
|
int counter;
|
|
double time_so_far;
|
|
|
|
public:
|
|
|
|
/*
|
|
* Constructor for a CRewardCumulative object.
|
|
*/
|
|
CRewardCumulative(int rsi, double time);
|
|
|
|
/*
|
|
* Destructor for a CRewardCumulative object.
|
|
*/
|
|
~CRewardCumulative();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method determines whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
void Notify_State(CPathState* last_state, int* current_state);
|
|
|
|
/*
|
|
* Returns a string representation of this CRewardCumulative object.
|
|
*/
|
|
string To_String();
|
|
|
|
/*
|
|
* Resets the counter, time_so_far and answer_double and calls the superclass
|
|
* Reset() method.
|
|
*/
|
|
void Reset();
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula. This
|
|
* will *only* be if the answer has been proven, *not* if the path is looping.
|
|
*/
|
|
bool Is_Answer_Known(CLoopDetectionHandler* loop_detection); //must override this because do not want looping to stop verification
|
|
|
|
void Write_Formula(int fd);
|
|
};
|
|
|
|
/*
|
|
* CRewardInstantanious
|
|
* ====================
|
|
*
|
|
* The CRewardCumulative class is used to store and deal with rewards formulae
|
|
* of the form:
|
|
* [ I time ].
|
|
* i.e. What is the instantaneous state reward at the given time.
|
|
*
|
|
*/
|
|
class CRewardInstantanious : public CRewardFormula
|
|
{
|
|
private:
|
|
double time;
|
|
int counter;
|
|
double time_so_far;
|
|
|
|
public:
|
|
|
|
/*
|
|
* Constructor for a CRewardInstantaneous object...and yes it does set the
|
|
* time_so_far variable to 0.0 now... ooops
|
|
*/
|
|
CRewardInstantanious(int rsi, double time);
|
|
|
|
/*
|
|
* Destructor for a CRewardInstantaneous object.
|
|
*/
|
|
~CRewardInstantanious();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method determines whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
void Notify_State(CPathState* last_state, int* current_state);
|
|
|
|
/*
|
|
* Returns a string representation of this CRewardInstantaneous object.
|
|
*/
|
|
string To_String();
|
|
|
|
/*
|
|
* Resets the counter, time_so_far and answer_double variables and calls the superclass
|
|
* Reset() method.
|
|
*/
|
|
void Reset();
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula. This
|
|
* will *only* be if the answer has been proven, *not* if the path is looping.
|
|
*/
|
|
bool Is_Answer_Known(CLoopDetectionHandler* loop_detection); //must override this because do not want looping to stop verification
|
|
|
|
void Write_Formula(int fd);
|
|
};
|
|
|
|
/*
|
|
* CRewardReachability
|
|
* ===================
|
|
*
|
|
* The CRewardReachability class is used to store and deal with rewards formulae
|
|
* of the form:
|
|
* [ F expression ].
|
|
* i.e. What is the accumulated reward when expression is satisfied.
|
|
*
|
|
*/
|
|
class CRewardReachability : public CRewardFormula
|
|
{
|
|
private:
|
|
CExpression* expression;
|
|
|
|
public:
|
|
|
|
/*
|
|
* Constructor for a CRewardReachability object.
|
|
*/
|
|
CRewardReachability(int rsi, CExpression* expression);
|
|
|
|
/*
|
|
* Destructor for a CRewardReachability object.
|
|
*/
|
|
~CRewardReachability();
|
|
|
|
/*
|
|
* This method should be called for each update to the current state. This
|
|
* method determines whether the answer can be determined for this update
|
|
* and if, so calculates the answer and puts it in the answer member variable.
|
|
*/
|
|
void Notify_State(CPathState* last_state, int* current_state);
|
|
|
|
/*
|
|
* Returns a string representation of this CRewardReachability object.
|
|
*/
|
|
string To_String();
|
|
|
|
/*
|
|
* Determines whether the answer is already known for this path formula. This
|
|
* will either be if the answer has been proven, or if the path is looping.
|
|
* If the path is looping, this method also sets the answer_double to undefined
|
|
* because the reward is infinite.
|
|
*/
|
|
bool Is_Answer_Known(CLoopDetectionHandler* loop_detection);
|
|
|
|
void Write_Formula(int fd);
|
|
};
|
|
|
|
|
|
|
|
//=============================================================================
|
|
// Function Declarations
|
|
//=============================================================================
|
|
|
|
/**
|
|
* This function removes all registered path formulae
|
|
* from memory.
|
|
*/
|
|
void Deallocate_PCTL_Core();
|
|
|
|
/*
|
|
* Allocates storage for path formulae to be registered.
|
|
*/
|
|
void Allocate_PCTL_Core();
|
|
|
|
/*
|
|
* Adds the given path formula to registered_path_formula.
|
|
*/
|
|
int Register_Path_Formula(CPathFormula* formula);
|
|
|
|
/*
|
|
* Returns the index of the formula parameter in registered_path_formula
|
|
*/
|
|
int Index_Of_Path_Formula(CPathFormula* formula);
|
|
|
|
/*
|
|
* Calls the Notify_State method of each path or reward formula in
|
|
* registered_path_formulae.
|
|
*/
|
|
void Notify_Path_Formulae(CPathState* last_state, int* current_state, CLoopDetectionHandler* loop_detection);
|
|
|
|
//TODO move this to path PCTL manager
|
|
|
|
/*
|
|
void Recalculate_Path_Formulae();*/
|
|
|
|
/*
|
|
* Resets each path or reward formula in registered_path_formulae for
|
|
* new calculations.
|
|
*/
|
|
void Reset_Path_Formulae();
|
|
|
|
/*
|
|
* Method for direct querying of a registered path formula.
|
|
* Returns -1 if the answer is not known (or an error)
|
|
* Returns 0 if the answer is known as false
|
|
* Returns 1 if the answer is known as true
|
|
* Returns 2 if the answer is numeric.
|
|
*/
|
|
int Query_Path_Formula(int index);
|
|
|
|
/*
|
|
* If the path formula at the index is numeric, this returns the answer
|
|
*/
|
|
double Query_Path_Formula_Numeric(int index);
|
|
|
|
/*
|
|
* Outputs the contents of registered_path_formulae to the command line.
|
|
*/
|
|
void Print_Formulae();
|
|
|
|
CPathFormula* Get_Path_Formula(int index);
|
|
|
|
//==============================================================================
|
|
// IO Functions
|
|
//==============================================================================
|
|
|
|
void Write_Pctl_Manager(int fd);
|
|
|
|
void Read_Pctl(int fd);
|
|
|
|
CPathFormula* Read_Path_Formula(int fd);
|
|
|
|
#endif
|