RandomGenerator (Averest)

RandomGenerator Module

Namespace: Averest.TeachingTools
Assembly: Averest.dll

This module implements

Functions and values

Function or value	Description
`IntuitionisticLogic2CTL phi` Full Usage: `IntuitionisticLogic2CTL phi` Parameters: phi : `BoolExpr` Returns: `SpecExpr`	translation of intuitionistic logic formulas to equivalent CTL formulas phi : `BoolExpr` Returns: `SpecExpr`
`PrintTeachingToolKripke ostr kripke` Full Usage: `PrintTeachingToolKripke ostr kripke` Parameters: ostr : `TextWriter` kripke : `KripkeStructureExpl`	print teaching tool input for a given Kripke structure ostr : `TextWriter` kripke : `KripkeStructureExpl`
`PrintTeachingToolParityGame ostr pg` Full Usage: `PrintTeachingToolParityGame ostr pg` Parameters: ostr : `TextWriter` pg : `ParityGame`	print teaching tool input for a given parity game ostr : `TextWriter` pg : `ParityGame`
`RandomAutomataDeterminizationExamples rand inVars stVars stLen trLen numProblems` Full Usage: `RandomAutomataDeterminizationExamples rand inVars stVars stLen trLen numProblems` Parameters: rand : `Random` inVars : `string list` stVars : `string list` stLen : `int` trLen : `int` numProblems : `int`	generate random symbolic representations of automata and determinize them rand : `Random` inVars : `string list` stVars : `string list` stLen : `int` trLen : `int` numProblems : `int`
`RandomBddAlgorithmExamples rand varL numOps numProblems` Full Usage: `RandomBddAlgorithmExamples rand varL numOps numProblems` Parameters: rand : `Random` varL : `string list` numOps : `int` numProblems : `int`	generate a Latex file for BDD algorithm example computations rand : `Random` varL : `string list` numOps : `int` numProblems : `int`
`RandomCTL rand varL length` Full Usage: `RandomCTL rand varL length` Parameters: rand : `Random` varL : `string seq` length : `int` Returns: `SpecExpr`	generate a random CTL formula rand : `Random` varL : `string seq` length : `int` Returns: `SpecExpr`
`RandomFutureLTL rand varL length` Full Usage: `RandomFutureLTL rand varL length` Parameters: rand : `Random` varL : `string array` length : `int` Returns: `SpecExpr`	generate a random LTL formula with only future operators rand : `Random` varL : `string array` length : `int` Returns: `SpecExpr`
`RandomFutureLTLwithoutPropLogic rand varL length` Full Usage: `RandomFutureLTLwithoutPropLogic rand varL length` Parameters: rand : `Random` varL : `string array` length : `int` Returns: `SpecExpr`	generate a random future LTL formula without propositional logic rand : `Random` varL : `string array` length : `int` Returns: `SpecExpr`
`RandomGeneratorTool qscoll` Full Usage: `RandomGeneratorTool qscoll` Parameters: qscoll : `NameValueCollection`	teaching tool to be called by the cgi-interface qscoll : `NameValueCollection`
`RandomKripkeStructure trProb rand varL numStates` Full Usage: `RandomKripkeStructure trProb rand varL numStates` Parameters: trProb : `float` rand : `Random` varL : `string seq` numStates : `int` Returns: `KripkeStructureExpl`	generate a random Kripke structure trProb : `float` rand : `Random` varL : `string seq` numStates : `int` Returns: `KripkeStructureExpl`
`RandomLinearInequalities rand withInt numEqs numVars maxCoeff numProblems maxSteps` Full Usage: `RandomLinearInequalities rand withInt numEqs numVars maxCoeff numProblems maxSteps` Parameters: rand : `Random` withInt : `bool` numEqs : `int` numVars : `int` maxCoeff : `int` numProblems : `int` maxSteps : `'a`	rand : `Random` withInt : `bool` numEqs : `int` numVars : `int` maxCoeff : `int` numProblems : `int` maxSteps : `'a`
`RandomModelCheckingExamples trProb rand varL numStates numProblems` Full Usage: `RandomModelCheckingExamples trProb rand varL numStates numProblems` Parameters: trProb : `float` rand : `Random` varL : `string seq` numStates : `int` numProblems : `int`	generate a Latex file of CTL model checking problems trProb : `float` rand : `Random` varL : `string seq` numStates : `int` numProblems : `int`
`RandomParityGame trProb rand maxRank numStates` Full Usage: `RandomParityGame trProb rand maxRank numStates` Parameters: trProb : `float` rand : `Random` maxRank : `int` numStates : `int` Returns: `ParityGame`	generate a random Parity game trProb : `float` rand : `Random` maxRank : `int` numStates : `int` Returns: `ParityGame`
`RandomParityGameSolutions trProb rand maxRank numStates numProblems` Full Usage: `RandomParityGameSolutions trProb rand maxRank numStates numProblems` Parameters: trProb : `float` rand : `Random` maxRank : `int` numStates : `int` numProblems : `int`	trProb : `float` rand : `Random` maxRank : `int` numStates : `int` numProblems : `int`
`RandomPastLTL rand varL length` Full Usage: `RandomPastLTL rand varL length` Parameters: rand : `Random` varL : `string[]` length : `int` Returns: `SpecExpr`	generate a random LTL formula with past operators rand : `Random` varL : `string[]` length : `int` Returns: `SpecExpr`
`RandomPropLogic rand varL length` Full Usage: `RandomPropLogic rand varL length` Parameters: rand : `Random` varL : `BoolExpr[]` length : `int` Returns: `BoolExpr`	rand : `Random` varL : `BoolExpr[]` length : `int` Returns: `BoolExpr`
`RandomPropLogicExamples rand varL numOps numProblems` Full Usage: `RandomPropLogicExamples rand varL numOps numProblems` Parameters: rand : `Random` varL : `string seq` numOps : `int` numProblems : `int`	generate a Latex file for BDD/FDD/ZDD conversions and SAT Solving rand : `Random` varL : `string seq` numOps : `int` numProblems : `int`
`RandomPropLogicHilbert rand varL length` Full Usage: `RandomPropLogicHilbert rand varL length` Parameters: rand : `Random` varL : `BoolExpr[]` length : `int` Returns: `BoolExpr`	rand : `Random` varL : `BoolExpr[]` length : `int` Returns: `BoolExpr`
`RandomSatLTL rand withDet varL length numProblems` Full Usage: `RandomSatLTL rand withDet varL length numProblems` Parameters: rand : `Random` withDet : `bool` varL : `string array` length : `int` numProblems : `int`	generate random LTL formulas (without propositional operators) and compute a satisfying and an unsatisfying model rand : `Random` withDet : `bool` varL : `string array` length : `int` numProblems : `int`
`RandomSimulationExamples trProb rand varL numStates numProblems` Full Usage: `RandomSimulationExamples trProb rand varL numStates numProblems` Parameters: trProb : `float` rand : `Random` varL : `string seq` numStates : `int` numProblems : `int`	generate a Latex file of (bi)simulation problems trProb : `float` rand : `Random` varL : `string seq` numStates : `int` numProblems : `int`
`RandomSymbolicPreSucExamples rand varL stLen trLen numProblems` Full Usage: `RandomSymbolicPreSucExamples rand varL stLen trLen numProblems` Parameters: rand : `Random` varL : `string list` stLen : `int` trLen : `int` numProblems : `int`	rand : `Random` varL : `string list` stLen : `int` trLen : `int` numProblems : `int`
`RandomThmLTL rand varL length numTheorems` Full Usage: `RandomThmLTL rand varL length numTheorems` Parameters: rand : `Random` varL : `string array` length : `int` numTheorems : `int`	generate a Latex file with randomly generated LTL theorems rand : `Random` varL : `string array` length : `int` numTheorems : `int`