Shared Modules

project.py - Abstraction layer for project files

This module exposes an object that allows for simplified loading of the various files included in a single project.

class project.Project

A project object.

determineEnabledPropositions()

Populate lists all_sensors, enabled_sensors, etc.

getFilenamePrefix()

Returns the full path of most project files, minus the extension.

For example, if the spec file of this project is /home/ltlmop/examples/test/test.spec then this function will return /home/ltlmop/examples/test/test

getStrategyFilename()

Returns the full path of the file that should contain the strategy for this specification.

loadProject(spec_file)

Because the spec_file contains references to all other project files, this is all we need to know in order to load everything in.

loadRegionFile(decomposed=False)

Returns a Region File Interface object corresponding to the regions file referenced in the spec file

loadRegionMapping()

Takes the region mapping data and returns region mapping dictionary.

loadSpecFile(spec_file)

setSilent(silent)

writeSpecFile(filename=None)

regions.py - Regions Module

A simple module that defines a class for describing and manipulating rectangular and polygonal regions.

This is completely free software; please feel free to adapt or use this in any way you like.

Some parts extracted from pySketch by Erik Westra (ewestra@wave.co.nz)

class regions.Color(red=0, green=0, blue=0)

Blue()

Green()

Red()

SetFromName(name)

class regions.Point(x, y)

class regions.Region(type=1, position=Point(0.000000, 0.000000), size=Point(0.000000, 0.000000), height=0, color=None, points=None, name='')

A rectangular or polygonal region, defined by the following properties:

• ‘name’ Region name

• ‘type’ What type of region this is (rect or poly)

• ‘position’ The position of the object within the document

  (i.e., the top-left corner of the region’s bounding-box)

• ‘size’ The size of the object’s bounding box

• ‘color’ Color to use for drawing the region

• ‘pointArray’ Polygon points, relative to region position (stored in CW order)

• ‘alignmentPoints’ True/False array indicating for each vertex whether or not to use it as an alignment point

• ‘isObstacle’ Boolean value indicating whether the region should be treated as an obstacle

NOTE: All coordinates are stored internally with (0,0) at the top left.

X increases to right, and Y increases downwards.

addPoint(point, index)

Insert a new point at a given index, converting object type if necessary

faceAndFaceIntersection(face1, face2)

findPointsNear(face, center, distance)

findRegionNear(distance, mode='underEstimate', name='newRegion')

Given a region object and a distance value, return a new region object which covers the area that is within the ‘distance’ away from the given region.

getCenter()

Find the ‘center’ of a region

getData()

Return a copy of the object’s internal data. This is used for undo and to save this region to disk.

getDirection()

Determine convexity/concavity and the order of the points stored in the pointArray. For details on the algorithm, please refer to:

http://local.wasp.uwa.edu.au/~pbourke/geometry/clockwise/index.html

getFaces(includeHole=False)

Wrapper function to allow for iteration over faces of regions. A face is a frozenset of the two points (in absolute coordinates) that make up the face.

getPoints(relative=False, hole_id=None)

Wrapper function to allow for iteration over the points of a region without worrying about whether it’s a RECT or POLY. When hole_id is None, the boundary points of the region will be returned When Otherwise the points of holeList[hole_id] will be returned

getSelectionHandleContainingPoint(x, y, boundFunc=None)

Return the selection handle containing the given point, if any.

We return one of the predefined selection handle ID codes (defined at top).

objectContainsPoint(x, y)

Returns True iff this object contains the given point.

This is used to determine if the user clicked on the object.

objectWithinRect(x, y, width, height)

Return True iff this object falls completely within the given rect.

polyContainsPoint(poly_pts, x, y)

recalcBoundingBox()

Recalculate the bounding box for our object

removePoint(index)

Remove the point at the given index, converting object type if necessary

setData(data)

Set the object’s internal data.

‘data’ is a copy of the object’s saved data, as returned by getData() above. This is used for undo and to restore a previously saved region.

setDataOld(data)

Set the object’s internal data.

‘data’ is a copy of the object’s saved data, as returned by previous version of region editor. This function is only for backwards compatibility and will eventually be removed.

class regions.RegionFileInterface(background='None', regions=None, transitions=None)

A wrapper class for handling collections of regions and associated metadata.

Overview of exposed data structures:

• background (string): relative path of background image file

• regions (list): list of Region objects, with properties defined below

• transitions (list of lists):

  • key1 = Region object index
  • key2 = Region object index
  • values = Lists of faces connecting the two regions

getBoundingBox()

getCalibrationPoints()

getExternalFaces()

Returns a list of faces that are not connected to any other region on the map.

Generally, this only makes sense for maps that have already been decomposed.

getMaximumHeight()

getNextAvailableRegionNumber()

Look for the smallest region name of form r1, r2, ... available.

indexOfRegionWithName(name)

readFile(filename)

For file format information, refer to writeFile() above.

recalcAdjacency()

Calculate the region adjacency matrix and a list of shared faces

Returns a list of shared faces

setToDefaultName(region)

splitSubfaces(obj1, obj2)

If we have a face of region obj1 that overlaps with the face of another region obj2, (i.e. the obj1 face is collinear with and has at least one point on the obj2 face) we split the larger face into two or three parts as appropriate.

writeFile(filename)

File format is described inside the comments variable.

class regions.Size(w, h)

GetHeight()

GetWidth()

regions.findRegionBetween(regionA, regionB, name='newRegion')

Find the region between two given regions (doesn’t include the given regions)

regions.pointLineIntersection(pt1, pt2, test_pt)

Given two points (pt1, pt2), find the point on the line formed by those points that is nearest to test_pt and give the distance.

class regions.prettierJSONEncoder(skipkeys=False, ensure_ascii=True, check_circular=True, allow_nan=True, sort_keys=False, indent=None, separators=None, encoding='utf-8', default=None)

Subclass of JSONEncoder that stops indenting after 2 levels; only seems to work well with python2.6 version, not 2.7 :(

fileMethods.py - File Access Methods

Some routines for reading and writing plaintext config/data files, shared throughout the toolkit.

fileMethods.properCase(str)

Returns a copy of a string, with the first letter capitalized and all others lower-case (CURRENTLY DOES NOTHING, and I’m not sure why that change was made)

fileMethods.readFromFile(fileName)

A simple method for reading in data from text files of the following format:

========= SECTION1 ==========

# COMMENT

HEADER1: # COMMENT
DATA1
DATA2

HEADER2: # COMMENT
DATA3

========= SECTION2 ===========

HEADER1:
DATA1

Given a file with the above contents, the function will return the following dictionary of dictionaries:

{ 'SECTION1' : { 'HEADER1': ['DATA1', 'DATA2'],
                 'HEADER2': ['DATA3'] },
{ 'SECTION2' : { 'HEADER1': ['DATA1'] } }

NOTE:

• Headers must be followed by a colon
• Section names must have at least one equals sign on both sides
• Dictionary keys will always be normalized so that only the first letter is capitalized (CURRENTLY DISABLED)
• All items are returned as strings and should be cast to the appropriate type before use, if appropriate
• Lines beginning with # are treated as comments
• Blank lines at the end of sections are ignored
• Any data without a section title will be returned under the empty string key: ''
• If no section titles are present, the outer dictionary will be ommitted

fileMethods.writeToFile(fileName, data, comments={})

A simple method for writing data to text files of the format described in the readFromFile() function above.

All data will be output in key-sorted order for the sake of consistency.

Any items in the comments hash whose keys match those of the data hash will be included as comments in the appropriate section of the file.

If it exists, the comment keyed as "FILE_HEADER" will be added to the top of the output file.

parseEnglishToLTL.py - Structured English to LTL Translator

Module that parses a set of structured English sentences into the corresponding LTL subformulas.

parseEnglishToLTL.bitEncoding(numRegions, numBits)

This function creates a dictionary that contains the bit encoding for the current and next region. Takes number of regions and returns a dictionary with ‘current’ and ‘next’ as keys, each containing a list of the respective encodings.

parseEnglishToLTL.createStayFormula(regionNames, use_bits=True)

parseEnglishToLTL.nextify(p)

parseEnglishToLTL.parseAfterEachTime(Cond, Requirement, sensorProp, allRobotProp, lineInd, StayFormula)

parseEnglishToLTL.parseCond(condition, sensorList, allRobotProp, ReqType, lineInd)

This function creates the LTL formula representing the condition part of a conditional. It takes the condition and PropList - a list of propositions (to check that only ‘legal’ propositions are used)and ‘lineInd’ that indicates which line is being processed. Returns the LTL formula as a string.

parseEnglishToLTL.parseConditional(Condition, ReqFormulaInfo, CondType, sensorList, allRobotProp, lineInd)

This function creates the LTL formula representing a conditional. It takes the condition, the requirement formula (that was already parsed), the condition type, and the list of all propositions (to check that only ‘legal’ propositions are used) and ‘lineInd’ that indicates which line is being processed. Returns a dictionary with 2 keys: ‘formula’ containing the LTL formula as a string and ‘type’ containing the type of the requirement.

parseEnglishToLTL.parseEvent(EventProp, SetEvent, ResetEvent, sensorProp, RobotProp, lineInd)

This function creates the LTL formulas encoding when a proposition should be true and when false. This is used as a macro to define ‘memory’ propositions. It takes the proposition, the boolean formulas defining the set and reset events, the propositions (to check that only ‘legal’ propositions are used) and ‘lineInd’ that indicates which line is being processed. Returns the LTL formula as a string.

parseEnglishToLTL.parseInit(sentence, PropList, lineInd)

This function creates the LTL formula representing the initial conditions. It takes the sentence and PropList - a list of propositions (to check that only ‘legal’ propositions are used) and ‘lineInd’ that indicates which line is being processed. Returns the LTL formula as a string.

parseEnglishToLTL.parseLiveness(sentence, sensorList, allRobotProp, lineInd)

This function creates the LTL formula representing a basic liveness requirement. It takes the sentence, the sensor list and the list of all robot propositions (to check that only ‘legal’ propositions are used and to determine whether it is an environment safety or a robot one) and ‘lineInd’ that indicates which line is being processed. Returns a dictionary with 2 keys: ‘formula’ containing the LTL formula as a string and ‘type’ containing either ‘EnvGoals’ or ‘SysGoals’.

parseEnglishToLTL.parseSafety(sentence, sensorList, allRobotProp, lineInd)

This function creates the LTL formula representing a basic safety requirement. It takes the sentence, the sensor list and the list of all robot propositions (to check that only ‘legal’ propositions are used and to determine whether it is an environment safety or a robot one) and ‘lineInd’ that indicates which line is being processed. Returns a dictionary with 2 keys: ‘formula’ containing the LTL formula as a string and ‘type’ containing either ‘EnvTrans’ or ‘SysTrans’.

parseEnglishToLTL.parseToggle(EventProp, ToggleEvent, sensorProp, RobotProp, lineInd)

This function creates the LTL formulas encoding when a proposition’s value should toggle (T->F, F->T). It takes the proposition, the boolean formula defining the toggle event, the propositions (to check that only ‘legal’ propositions are used) and ‘lineInd’ that indicates which line is being processed. Returns the LTL formula as a string.

parseEnglishToLTL.replaceLogicOp(formula)

This function replaces the logic operators with TLV convention.

parseEnglishToLTL.replaceRegionName(formula, bitEncode, regionList)

This function replaces the region names with the appropriate bit encoding.

parseEnglishToLTL.writeSpec(text, sensorList, regionList, robotPropList)

This function creates the Spec dictionary that contains the parsed LTL subformulas. It takes the text that contains the structured English, the list of sensor propositions, the list containing the region names and the list of robot propositions (other than regions).

createJTLVinput.py - LTL Pre-Processor Routines

Module that creates the input files for the JTLV based synthesis algorithm. Its functions create the skeleton .smv file and the .ltl file which includes the topological relations and the given spec.

createJTLVinput.createInitialRegionFragment(regions, use_bits=True)

createJTLVinput.createLTLfile(fileName, spec_env, spec_sys)

This function writes the LTL file. It encodes the specification and topological relation. It takes as input a filename, the list of the sensor propositions, the list of robot propositions (without the regions), the adjacency data (transition data structure) and a specification

createJTLVinput.createNecessaryFillerSpec(spec_part)

Both assumptions guarantees need to have at least one each of initial, safety, and liveness. If any are not present, create trivial TRUE ones.

createJTLVinput.createSMVfile(fileName, sensorList, robotPropList)

This function writes the skeleton SMV file. It takes as input a filename, the number of regions, the list of the sensor propositions and the list of robot propositions (without the regions).

createJTLVinput.createTopologyFragment(adjData, regions, use_bits=True)

createJTLVinput.flattenLTLFormulas(f)

class asyncProcesses.AsynchronousProcessThread(cmd, callback, logFunction)

kill()

run()

class decomposition.decomposition(polygon, holes=[])

MP5()

calcAngle(a, b, c)

A function that calculates the angle between 0 and 2*pi rad swept by a counterclockwisr rotation from line segment ba to bc

a,b,c are vertices Return True when the angle is smaller than or equals pi Return False when the angle is larger than pi .

checkNextPoly(allVertices)

checkPointInside(allVertices)

True: There is at least one vertex inside the polygon generated False: There is no vertex inside

drawPoly(polyList, fileName)

findInitialVertex(allVertices)

Find notch vertex to start

allVertices: List of all vertices of the polygon to be decomposed

getFaces(poly)

Wrapper function to allow for iteration over faces of regions. A face is a tuple of the two points (in absolute coordinates) that make up the face, sorted so that a given face is defined uniquely.

FIXME: Make sure we take advantage of this uniqueness elsewhere; I think we check too many conditions sometimes

getVertices(poly)

lineLineIntersection(l1p1, l1p2, l2p1, l2p2)

linePolyIntersection(poly, vertexA, vertexB, boundaryPoly)

mergeHole(allVertices, initialIndex, holeIndex, vertexIndex)

pointPointDistance(pt1, pt2)

removeContour(contour)

reversePolyOrientation(poly)

class decomposition.myVertex(x=0, y=0)

decomposition.removeDuplicatePoints(points)

handlerSubsystem.py - Interface for working with handlers, configs

class handlerSubsystem.HandlerSubsystem(executor, project_root_dir)

Interface dealing with configuration files and handlers

createHandlerMethodConfig(robot_name, handler_name, method_name, kwargs)

Create a handler method config object from the given information of this method

createPropositionMappingExecutionFunctionFromString(func_string, mode)

Given a string description of the function(s) that some proposition maps to, create the appropriate HandlerMethodConfigs and return the function that will evaluate their execute() methods.

findHandlerTypeStringFromName(handler_name)

given a handler name, find folder of this handler in the handlers/share folder

getDefaultPropMapping(sensor_prop_list, actuator_prop_list)

Return the default proposition mapping based on the propositions given

getHandlerConfigDefault(r_type, h_type, h_name)

Get default handler config object from handler_configs if exists Or load it from corresponding file if not exits given rtype (str: share or robot type (str)), htype (class), h_name (str). NOT yet overridden by .robot defaults

getHandlerInstanceByName(handler_name)

Return the instantiated handler object for a given name or None if it is not instantiated

getHandlerInstanceByType(handler_type_class, robot_name='')

Return the handler instance of the given handler type When no robot_name is given, the handler is assumed to be of the main robot When the handler type is either sensor or actuator, a robot_name is required Return None if the handler instance cannot be found

getMainRobot()

Return the main robot of the current executing config

getPose(cached=False)

A wrapper function that returns the pose from the pose handler of the main robot in the current executing config

getRobotByType(t)

Assume only one robot is loaded per type

getSensorValue(prop_name_list)

given a list of proposition names, return dictionary with {prop_name:sensor_value}, where sensor_value is a boolean value returned by sensor handler

gotoRegion(current_region, next_region)

a wrapper function that set the target region to the motionControl handler of the main robot

initializeAllMethods()

initialize all method in self.prop2func mapping with initial=True

instantiateAllHandlers()

instantiate all the handlers of the main robot of the current executing config instantiate only the init handler of the non-main robot

loadAllConfigFiles()

Load all experiment config files in the project/configs folder

loadAllHandlers()

Load all handlers in the handler folder

loadAllRobots()

Load all robot files in each handlers/robot_type folder

loadConfigFile(file_name)

Load the given experiment config file in the project/configs folder

loadHandler(r_type, h_type, h_name)

Load the handler config object from the file based on the given info

method2String(method_config, robot_name='')

Return the string representation according to the input method config

prepareHandler(handler_config)

Instantiate the handler object of the given handler config if it is not already instantiated Return the handler instance

prepareMapping()

prepare the python objects corresponding to each proposition stored in the prop_mapping of current config object

saveAllConfigFiles()

setActuatorValue(actuator_state)

given a dictionary with {prop_name:actuator_value}, where actuator_value is a boolean value that gets passed to actuator handler

setExecutingConfig(config_object_name)

set the current executing config to the experiment config with the given name if the given config cannot be found, try to load it first

setVelocity(x, y)

a wrapper function that set the velocity to the drive handler of the main robot

string2Method(method_string, robots)

Return the HandlerMethodConfig according to the input string from configEditor This functions must be located in HandlerSubsystem in order to get access to handler_configs dictionary

method_string: a string that stores the information of a method configObj

for example: a = “nao_maeby.NaoSensorHandler.seePerson(name=’nao’, test=[1,2,3])”

robots: a list of robots in the current experiment config. we need this to find the robot type and avaliable handlers

based on robot_name

class mapRenderer.DrawableRegion(*args, **kwds)

Extends the Region class to allow drawing.

draw(dc, pdc, selected, scale=1.0, showAlignmentPoints=True, highlight=False, deemphasize=False)

Draw this Region into our window.

‘dc’ is the device context to use for drawing. If ‘selected’ is True, the object is currently selected and should be drawn as such.

classmethod fromRegion(region)

mapRenderer.drawMap(target, rfi, scaleToFit=True, drawLabels=True, highlightList=, []deemphasizeList=, []memory=False, showBits=False)

Draw the map contained in the given RegionFileInterface onto the target canvas.

class parseLP.parseLP

A parser to parse the locative prepositions in specification

checkOverLapping()

Check if and regions overlap each other Break the ones that overlap into portions that don’t overlap

decomp()

Decompose the region with holes or are concave

decomposeWithOverlappingPoint(polygon)

When there are points overlapping each other in a given polygon First decompose this polygon into sub-polygons at the overlapping point

drawAllPortions()

Output a drawing of all the polygons that stored in self.portionOfRegion, for debug purpose

generateNewRegion()

Generate new regions for locative prepositions

intAllPoints(poly)

Function that turn all point coordinates into integer Return a new polygon

main(argv)

Main function; run automatically when called from command-line

removeSmallRegions()

A function to remove small region

saveRegions(fileName='')

Save the region data into a new region file

class resynthesis.ExecutorResynthesisExtensions

Extensions to Executor to allow for specification rewriting and resynthesis. This class is not meant to be instantiated.

getCurrentStateAsLTL(include_env=False)

Return a boolean formula (as a string) capturing the current discrete state of the system (and, optionally, the environment as well)

resynthesizeFromNewSpecification(spec_text)

class specCompiler.SpecCompiler(spec_filename=None)

abortSynthesis()

Kill any running synthesis process.

compile()

loadSimpleSpec(text='', regionList=, []sensors=, []actuators=, []customs=, []adj=, []outputfile='')

Load a simple spec given by the arguments without reading from a spec file

For Slurp

region, sensors, actuators, customs are lists of strings representing props adj is a list of tuples [(region1,region2),...]

loadSpec(spec_filename)

Load the project object

ltlConjunctsFromBadLines(to_highlight, useInitFlag)

postprocessLTL(text, sensorList, robotPropList)

prepareSlugsInput()

Convert from JTLV input format (.smv+.ltl) to Slugs input format (.slugsin) using the script provided by Slugs.

This is a stop-gap fix; eventually we should just produce the input directly instead of using the conversion script.

splitSpecIntoComponents(env, sys)

substituteMacros(text)

Replace any macros passed to us by the parser. In general, this is only necessary in cases where bitX propositions are needed, since the parser is not supposed to know about them.

unrealCores(cmd, topo, badStatesLTL, conjuncts, deadlockFlag)

unsatCores(cmd, topo, badInit, conjuncts, maxDepth, numRegions)

---

class strategy.Domain(name, value_mapping=None, endianness=0, num_props=None)

A Domain is a bit-vector abstraction, allowing a proposition to effectively have values other than just True and False.

Domain “x” consists of propositions “x_b0”, “x_b1”, “x_b2”, ..., and the

value of the domain corresponds to the interpretation of these propositions as a binary string (following the order specified by endianness). If value_mapping is specified, the numeric value of the domain will be used as an index into this array, and the corresponding element (must be non-integer) will be returned when the proposition value is queried, instead of a number (likewise, when setting the value of the proposition, this mapping will be used in reverse).

num_props can be used to specify the size of the vector; if not

specified, this will be automatically calculated based on the size of the value_mapping array.

Define a domain: >>> animals = [“cat”, “dog”, “red-backed fairywren”, “pseudoscorpion”, “midshipman”] >>> d = Domain(“favorite_animal”, animals)

Notice that by using a domain we’ve reduced the number of props necessary >>> assert d.num_props == 3

Conversion can go in both directions: >>> for value in animals: ... p = d.valueToPropAssignments(value) ... assert value == d.propAssignmentsToValue(p)

B0_IS_LSB = 1

B0_IS_MSB = 0

getPropositions()

Returns a list of the names of the propositions that are covered by this domain.

numericValueToPropAssignments(number)

Convert an integer value into the corresponding dictionary [prop_name(str)->value(bool)] of propositions composing this domain

propAssignmentsToNumericValue(prop_assignments)

Convert a dictionary [prop_name(str)->value(bool)] of propositions composing this domain into an integer value.

propAssignmentsToValue(prop_assignments)

Return the value of this domain, based on a dictionary [prop_name(str)->value(bool)] of the values of the propositions composing this domain.

valueToPropAssignments(value)

Convert a value into the corresponding dictionary [prop_name(str)->value(bool)] of propositions composing this domain

class strategy.State(parent, prop_assignments=None)

A state, at its most basic, consists of a value assignment to propositions (represented as a dictionary {proposition name (string) -> proposition value}).

Additional metadata can be attached as necessary.

When created, a reference to the parent StateCollection needs to be be passed so that the state is aware of its evaluation context.

For example usage, see the documentation for StateCollection.

A Note About Multi-Valent Propositions:

Multivalent propositions (i.e. those whose value can span a Domain), are

handled fairly flexibly internally, but most of the dynamic translation is hidden from the user.

In general, read access to propositions will always be presented at the

highest-level possible. For example, when asking for the value of a state, multivalent propositions are presented instead of the underlying binary subpropositions (unless explicitly overridden by using the expand_domains flag provided by some functions). That said, if one wishes to query the value of a subproposition for some reason, its value will be calculated automatically.

In a similar vein, in order to minimize the worries of those using this

module, multivalent propositions can be written to– and are stored internally– in one of two ways: either as multiple binary assignments to the subpropositions of the domain, or a single value assignment to the domain proposition itself. This latter form is preferred, since it is simplest, and internal accounting is biased in this direction.

getAll(expand_domains=False)

Return a dictionary of assignments to all propositions for this state.

If expand_domains is True, return only the binary subpropositions for domains instead of the usual multivalent proposition.

getInputs(expand_domains=False)

Return a dictionary of assignments to input propositions for this state.

If expand_domains is True, return only the binary subpropositions for domains instead of the usual multivalent proposition.

getLTLRepresentation(mark_players=True, use_next=False, include_inputs=True, swap_players=False)

Returns an LTL formula representing this state.

If mark_players is True, input propositions are prepended with “e.”, and output propositions are prepended with “s.”. (If swap_players is True, these labels will be reversed [this feature is used by Mopsy])

If use_next is True, all propositions will be modified by a single “next()” operator. include_env, which defaults to True, determines whether to include input propositions in addition to output propositions.

getName()

getOutputs(expand_domains=False)

Return a dictionary of assignments to output propositions for this state.

If expand_domains is True, return only the binary subpropositions for domains instead of the usual multivalent proposition.

getPropValue(name)

Return the value of the proposition name in this state.

(Note: expand_domains is not supported here because it would

entail returning multiple values. Use getPropValues() for that.)

getPropValues(names, expand_domains=False)

Return a dictionary of assignments to the propositions in names for this state.

If expand_domains is True, return only the binary subpropositions for domains instead of the usual multivalent proposition.

satisfies(prop_assignments)

Returns True iff the proposition settings in this state agree with all prop_assignments. Any unspecified propositions are treated as don’t-cares.

setPropValue(prop_name, prop_value)

Sets the assignment of propositions prop_name to prop_value in this state. A lot of sanity checking is performed to ensure the name and value are both appropriate.

setPropValues(prop_assignments)

Update the assignments in this state according to prop_assignments.

Any existing assignments to propositions not mentioned in prop_assignments are untouched.

class strategy.StateCollection(*args, **kwds)

StateCollection is a simple extension of list, to allow for keeping track of meta-information about states, such as which propositions are inputs and which are outputs, as well as domains. (These are not class properties of State because different StateCollections might have different settings.)

Create a new state collection: >>> states = StateCollection()

Define some basic true/false propositions: >>> states.addInputPropositions((“low_battery”,)) >>> states.addOutputPropositions((“hypothesize”, “experiment”, “give_up”))

Define some multi-valent propositions: >>> regions = [“kitchen”, “living”, “bedroom”] >>> animals = [“cat”, “dog”, “red-backed fairywren”, “pseudoscorpion”, “midshipman”] >>> states.addOutputPropositions([Domain(“region”, regions)]) >>> states.addInputPropositions([Domain(“nearby_animal”, animals, Domain.B0_IS_LSB)])

Create a new state: >>> test_assignment = {“region”: “bedroom”, “nearby_animal”: “midshipman”, ... “low_battery”: True, “hypothesize”: True, ... “experiment”:False, “give_up”:False} >>> s = states.addNewState(test_assignment) >>> assert s.satisfies(test_assignment)

You can also query and set the state values using low-level subpropositions: >>> s2 = states.addNewState(s.getAll(expand_domains=True)) >>> assert s2.satisfies(test_assignment)

LTL is available too! #>>> s2.getLTLRepresentation() #’!e.nearby_animal_b1 & !e.nearby_animal_b0 & e.nearby_animal_b2 & e.low_battery & s.region_b0 & !s.region_b1 & !s.give_up & !s.experiment & s.hypothesize’

addInputPropositions(prop_list)

Register the propositions in prop_list as input propositions. Each element of prop_list may be either a bare string, which is treated as the name of a binary proposition, or a Domain object, which indicates a multivalent proposition.

addNewState(prop_assignments=None, goal_id=None)

Create a new state with the assignment prop_assignment and goal ID goal_id and add it to the StateCollection.

Returns the new state.

addOutputPropositions(prop_list)

Register the propositions in prop_list as output propositions. Each element of prop_list may be either a bare string, which is treated as the name of a binary proposition, or a Domain object, which indicates a multivalent proposition.

clearPropositionsAndDomains()

Remove all propositions and domain definitions.

clearStates()

Remove all states.

expandDomainsInPropAssignment(prop_assignments)

Replace all domain propositions in the dictionary with their subpropositions

getDomainByName(name)

Returns the Domain object with name name.

If no such Domain is found, returns None.

getDomainOfProposition(prop_name)

Returns the Domain object for which proposition prop_name is a subproposition.

If no such Domain is found, returns None.

getPropositions(expand_domains=False)

Return a list of all known proposition names.

class strategy.Strategy

A Strategy object encodes a discrete strategy, which gives a system move in response to an environment move (or the reverse, in the case of a counterstrategy).

Only subclasses of Strategy should be used.

configurePropositions(input_propositions, output_propositions)

Set the input and output propositions for this strategy.

input_propositions and output_propositions must both be lists, consisting of any combination of strings (i.e. binary proposition names) and strategy.Domain objects (for multivalent propositions).

All existing definitions will be cleared.

This must be done before creating any states.

exportAsDotFile(filename, regionMapping, starting_states=None)

Output an explicit-state strategy to a .dot file of name filename. (For use with GraphViz.)

findTransitionableStates(prop_assignments, from_state=None)

Return a list of states that can be reached from from_state and satisfy prop_assignments. If from_state is omitted, the strategy’s current state will be used.

iterateOverStates()

Returns an iterator over all known states.

loadFromFile(filename)

Load a strategy from a file.

searchForOneState(prop_assignments, state_list=None)

Iterate through all known states (or a subset specified in state_list) and return the first one that matches prop_assignments.

Returns None if no such state is found.

searchForStates(prop_assignments, state_list=None)

Returns an iterator for the subset of all known states (or a subset specified in state_list) that satisfy prop_assignments.

strategy.TestLoadAndDump(spec_filename)

strategy.createStrategyFromFile(filename, input_propositions, output_propositions)

High-level method for loading a strategy of any type from file.

Takes a filename and lists of input and output propositions. Returns a fully-loaded instance of a Strategy subclass.

class fsa.FSAStrategy

An automaton object is a collection of state objects along with information about the current state of the automaton when being executed.

findTransitionableStates(prop_assignments, from_state=None)

Return a list of states that can be reached from from_state and satisfy prop_assignments. If from_state is omitted, the strategy’s current state will be used.

searchForStates(prop_assignments, state_list=None)

Returns an iterator for the subset of all known states (or a subset specified in state_list) that satisfy prop_assignments.

class bdd.BDDStrategy

BDDToPropAssignment(bdd, var_names)

BDDToState(bdd)

BDDToStates(bdd)

findTransitionableStates(prop_assignments, from_state=None)

Return a list of states that can be reached from from_state and satisfy prop_assignments. If from_state is omitted, the strategy’s current state will be used.

getAllVariableBDDs(use_next=False)

getAllVariableNames(use_next=False)

getBDDFromJx(jx)

getJxFromBDD(bdd)

prime(bdd)

printStrategy()

Dump the minterm of the strategy BDD. For debugging only.

propAssignmentToBDD(prop_assignments, use_next=False)

Create a BDD that represents the given binary proposition assignments (expressed as a dictionary from prop_name[str]->prop_val[bool]). If use_next is True, all variables will be primed.

satAll(bdd, var_names)

satOne(bdd, var_names)

searchForStates(prop_assignments, state_list=None)

Returns an iterator for the subset of all known states (or a subset specified in state_list) that satisfy prop_assignments.

stateListToBDD(state_list, use_next=False)

stateToBDD(state, use_next=False)

Create a BDD that represents the given state. If use_next is True, all variables will be primed.

unprime(bdd)