DREAM::ModelCheck Class Reference

Model check class. More...

#include <ModelCheck.h>

List of all members.

Public Member Functions
	ModelCheck (DREAM::System *system_ptr)
	Constructor.
	~ModelCheck ()
	Destructor.
bool	random_testing (DREAM::System *system_ptr, bool verbose)
	Random-tests the system.
bool	trace_based_model_check (DREAM::System *system_ptr, bool verbose) throw (DREAM::Exception)
	Simple proof-of-concept simulation-based model checker.
Private Member Functions
bool	branching_point (DREAM::NODE_AVLTREE *node_avltree, bool verbose)
	Used to generate cartesian cross-product of branching points.
Private Attributes
DREAM::System *	system_ptr_
	Pointer to the system.
double	endtoend_
	Stores the worst case end-to-end execution time encountered during the analysis.

---

Detailed Description

Model check class.

Provides methods to verify System designs.

Definition at line 62 of file ModelCheck.h.

---

Constructor & Destructor Documentation

DREAM::ModelCheck::ModelCheck

(

DREAM::System *

system_ptr

)

Constructor.

Definition at line 57 of file ModelCheck.cpp.

DREAM::ModelCheck::~ModelCheck

(

)

[inline]

Destructor.

Definition at line 69 of file ModelCheck.h.

---

Member Function Documentation

bool DREAM::ModelCheck::random_testing	(	DREAM::System *	system_ptr,
		bool	verbose
	)

Random-tests the system.

Do not underestimate this method!

Returns:

true if the system is schedulable

Parameters:

	system_ptr	is the pointer to the System.
	verbose	specifies whether output will be generated or not.

Definition at line 104 of file ModelCheck.cpp.

References DREAM::Solution::fitness(), Option::number_of_repetitions_, DREAM::repeat, DREAM::System::reset(), DREAM::System::simulate(), Option::verbose1_, and DREAM::System::visitor_map().

Referenced by main().

bool DREAM::ModelCheck::trace_based_model_check	(	DREAM::System *	system_ptr,
		bool	verbose
	)			throw (DREAM::Exception)

Simple proof-of-concept simulation-based model checker.

Model checks a distributed non-preemptive real-time system.

Returns:

true if the system is schedulable

Parameters:

	system_ptr	is the pointer to the System.
	verbose	specifies whether output will be generated or not.

Definition at line 193 of file ModelCheck.cpp.

References DREAM::AVLTree< key_type, item_type >::begin(), DREAM::Solution::deterministic(), DREAM::AVLTree< key_type, item_type >::end(), DREAM::Solution::fitness(), DREAM::AVLTree< key_type, item_type >::insert(), DREAM::System::reset(), DREAM::System::scheduler_map(), DREAM::System::simulate(), DREAM::AVLTree< key_type, item_type >::size(), Option::verbose1_, DREAM::System::visitor_map(), and DREAM::worstcase.

Referenced by main().

bool DREAM::ModelCheck::branching_point	(	DREAM::NODE_AVLTREE *	node_avltree,
		bool	verbose
	)			[private]

Used to generate cartesian cross-product of branching points.

Parameters:

	node_avltree	contains the Tasks to be manipulated.
	verbose	specifies whether output will be generated.

Definition at line 62 of file ModelCheck.cpp.

References DREAM::AVLTree< key_type, item_type >::begin(), DREAM::bestcase, Option::branching_, DREAM::branchingpoint, DREAM::System::destroy_priority_list(), DREAM::AVLTree< key_type, item_type >::end(), DREAM::System::inversion(), Option::race_condition_, system_ptr_, and DREAM::worstcase.

---

Member Data Documentation

DREAM::System* DREAM::ModelCheck::system_ptr_ [private]

Pointer to the system.

Definition at line 99 of file ModelCheck.h.

Referenced by branching_point().

double DREAM::ModelCheck::endtoend_ [private]

Stores the worst case end-to-end execution time encountered during the analysis.

Definition at line 102 of file ModelCheck.h.

---

The documentation for this class was generated from the following files:

• src/algorithm/ModelCheck.h
• src/algorithm/ModelCheck.cpp

---