prefltlf2pdfa package

Submodules

prefltlf2pdfa.prefltlf module

Module for handling preference LTLf formulas and converting them to preference automata.

This module utilizes the ltlf2dfa library to parse and process LTLf formulas into preference deterministic finite automata (PDFA). It also provides functions for validating and manipulating preference automata.

Note

The module checks for the presence of the mona tool, which is essential for translating LTLf to PDFA. If mona is not found, a warning message is printed to inform the user. In this case, the translate functionality may not work properly, but the remaining functions work okay.

class prefltlf2pdfa.prefltlf.PrefAutomaton[source]

Bases: object

add_class(cls_name)[source]
add_pref_edge(source_id, target_id)[source]
add_state(name)[source]
add_state_to_class(cls_id, q)[source]
add_transition(u, v, cond)[source]
classmethod deserialize(obj_dict)[source]
get_class_name(cls_id)[source]
get_state_id(name)[source]
get_states(data=False)[source]
serialize()[source]
class prefltlf2pdfa.prefltlf.PrefLTLf(spec, alphabet=None, **kwargs)[source]

Bases: object

Represents a PrefLTLf (Preference Linear Temporal Logic over Finite Traces) formula.

The class is used to define, parse, and serialize PrefLTLf specifications, as well as to translate the formulas into automata.

raw_spec

The raw specification of the PrefLTLf formula.

Type:

str

atoms

Set of atomic propositions appearing in the PrefLTLf specification.

Type:

set

alphabet

A list representing the alphabet for the specification, or None if not provided.

Type:

list

phi

A dictionary of LTLf formulas appearing in the PrefLTLf specification.

Type:

dict

relation

A set of triples (PREF_TYPE, LTLf, LTLf) constructed based on the given PrefLTLf specification.

Type:

set

Initializes the PrefLTLf formula.

Parameters:

  • spec (str) – The raw specification of the PrefLTLf formula.

  • alphabet (list, optional) – The alphabet for the specification (default is None).

  • **kwargs –

    Additional options for parsing and handling the formula.

    • skip_parsebool, optional

      If True, skips the parsing of the formula during initialization. Default is False.

    • auto_completestr, optional

      Specifies how the formula should handle incomplete preferences when parsing. The acceptable options are:

      • ”none”: No auto-completion. The formula must be fully specified, and any incompleteness will raise an error.

      • ”incomparable”: If preferences are incomplete, auto-completes them by marking certain conditions as incomparable.

      • ”minimal”: Auto-completes the preferences by adding the minimal number of relations needed to make the preferences complete.

      Default is “none”.

MAXIMAL_SEMANTICS = [<function semantics_mp_forall_exists>, <function semantics_mp_exists_forall>, <function semantics_mp_forall_forall>]
classmethod deserialize(obj_dict)[source]

Creates a PrefLTLf formula from a serialized dictionary.

Parameters:

obj_dict (dict) – A dictionary representing the serialized PrefLTLf formula.

Returns:

A new instance of the PrefLTLf formula.

Return type:

PrefLTLf

classmethod from_file(fpath, alphabet=None, auto_complete='none')[source]

Reads a PrefLTLf formula from a file.

Parameters:

  • fpath (str) – The file path to read the formula from.

  • alphabet (list, optional) – The alphabet for the specification (default is None).

  • auto_complete (str, optional) – The auto-completion method to use (default is “none”).

Returns:

A new instance of the PrefLTLf formula.

Return type:

PrefLTLf

parse(auto_complete='none')[source]

Parses the raw PrefLTLf formula and constructs the atomic propositions, relation, and LTLf formulas.

Parameters:

auto_complete (str, optional) – The method to use for auto-completion (default is “none”).

Returns:

A tuple containing - phi: Dictionary of {formula-id: LTLf Formula} - model: Set of binary relation of form (a, b) representing a is weakly preferred to b. - atoms: Set of strings representing atoms.

Return type:

tuple

serialize()[source]

Serializes the PrefLTLf formula into a JSON-compatible dictionary.

Returns:

A dictionary representing the serialized PrefLTLf formula.

Return type:

dict

translate(semantics=<function semantics_mp_forall_exists>, show_progress=False)[source]

Translates the PrefLTLf formula into a preference automaton under the given semantics.

Parameters:

  • semantics (function, optional) – The semantics function to use for translation (default is semantics_mp_forall_exists).

  • show_progress (bool, optional) – Whether to show progress during translation (default is False).

Returns:

The resulting preference automaton.

Return type:

PrefAutomaton

prefltlf2pdfa.semantics module

This module defines semantic evaluation functions for comparing two subsets of LTLf formulas given a preorder on LTLf formulas.

Functions:

  • semantics_forall_exists: Evaluates under “forall_exists” condition.

  • semantics_exists_forall: Evaluates under “exists_forall” condition.

  • semantics_forall_forall: Evaluates under “forall_forall” condition.

  • semantics_mp_forall_exists: Evaluates under “forall_exists” condition on maximal elements of two subsets of LTLf formulas.

  • semantics_mp_exists_forall: Evaluates under “exists_forall” condition on maximal elements of two subsets of LTLf formulas.

  • semantics_mp_forall_forall: Evaluates under “forall_forall” condition on maximal elements of two subsets of LTLf formulas.

prefltlf2pdfa.semantics.semantics_exists_forall(preorder, source, target)[source]

Check if there exists a formula in the source set such that all formulas in the target set satisfy the given preorder.

Parameters:

  • preorder (list of tuple) – The preorder defining the preference relation.

  • source (list) – List of binary values representing the source formulas.

  • target (list) – List of binary values representing the target formulas.

Returns:

True if the semantic condition is satisfied, False otherwise.

Return type:

bool

prefltlf2pdfa.semantics.semantics_forall_exists(preorder, source, target)[source]

Check if for all formulas in the source set, there exists a formula in the target set that satisfies the given preorder.

Parameters:

  • preorder (list of tuple) – The preorder defining the preference relation.

  • source (list) – List of binary values representing the source formulas.

  • target (list) – List of binary values representing the target formulas.

Returns:

True if the semantic condition is satisfied, False otherwise.

Return type:

bool

prefltlf2pdfa.semantics.semantics_forall_forall(preorder, source, target)[source]

Check if all formulas in the source set satisfy the preorder for all formulas in the target set.

Parameters:

  • preorder (list of tuple) – The preorder defining the preference relation.

  • source (list) – List of binary values representing the source formulas.

  • target (list) – List of binary values representing the target formulas.

Returns:

True if the semantic condition is satisfied, False otherwise.

Return type:

bool

prefltlf2pdfa.semantics.semantics_mp_exists_forall(preorder, source, target)[source]

Check if there exists a maximal outcome in the source set such that all maximal outcomes in the target set satisfy the given preorder.

This is a maximal-preorder variant of the semantics_exists_forall function, where the maximal outcomes of both the source and target sets are computed before evaluating the preorder condition.

Parameters:

  • preorder (list of tuple) – The preorder defining the preference relation.

  • source (list) – List of binary values representing the source formulas.

  • target (list) – List of binary values representing the target formulas.

Returns:

True if the semantic condition is satisfied, False otherwise.

Return type:

bool

See also

semantics_exists_forall: The base function for evaluating the condition. utils.maximal_outcomes: A utility function to compute maximal outcomes.

prefltlf2pdfa.semantics.semantics_mp_forall_exists(preorder, source, target)[source]

Check if for all maximal outcomes in the source set, there exists a maximal outcome in the target set that satisfies the given preorder.

This is a maximal-preorder variant of the semantics_forall_exists function, where the maximal outcomes of both the source and target sets are computed before evaluating the preorder condition.

Parameters:

  • preorder (list of tuple) – The preorder defining the preference relation.

  • source (list) – List of binary values representing the source formulas.

  • target (list) – List of binary values representing the target formulas.

Returns:

True if the semantic condition is satisfied, False otherwise.

Return type:

bool

See also

semantics_forall_exists: The base function for evaluating the condition. utils.maximal_outcomes: A utility function to compute maximal outcomes.

prefltlf2pdfa.semantics.semantics_mp_forall_forall(preorder, source, target)[source]

Check if all maximal outcomes in the source set satisfy the preorder for all maximal outcomes in the target set.

This is a maximal-preorder variant of the semantics_forall_forall function, where the maximal outcomes of both the source and target sets are computed before evaluating the preorder condition.

Parameters:

  • preorder (list of tuple) – The preorder defining the preference relation.

  • source (list) – List of binary values representing the source formulas.

  • target (list) – List of binary values representing the target formulas.

Returns:

True if the semantic condition is satisfied, False otherwise.

Return type:

bool

See also

semantics_forall_forall: The base function for evaluating the condition. utils.maximal_outcomes: A utility function to compute maximal outcomes.

prefltlf2pdfa.utils module

prefltlf2pdfa.utils.ltlf2dfa(ltlf_formula)[source]
prefltlf2pdfa.utils.maximal_outcomes(relation, outcomes)[source]
prefltlf2pdfa.utils.outcomes(dfa, q)[source]
prefltlf2pdfa.utils.vectorize(dfa, outcomes)[source]

prefltlf2pdfa.viz module

prefltlf2pdfa.viz.paut2base64(dot_semi_aut, dot_pref_graph)[source]

Convert the semi-automaton and preference graph images to base64 format. Useful for display on html pages.

Parameters:

  • dot_semi_aut (AGraph) – The DOT representation of the semi-automaton.

  • dot_pref_graph (AGraph) – The DOT representation of the preference graph.

Returns:

A tuple containing two base64 encoded strings (semi-automaton and preference graph).

Return type:

tuple

prefltlf2pdfa.viz.paut2dot(paut: PrefAutomaton, **kwargs)[source]

Generate images for semi-automaton and preference graph.

Parameters:

  • paut (PrefAutomaton) – The preference automaton to convert.

  • kwargs – Additional options for customizing the representation. - show_sa_state (bool): If True, display the state names in the semi-automaton; otherwise, use state IDs. - show_class (bool): If True, append the state class to the state names in the semi-automaton. - show_color (bool): If True, apply a color palette to the nodes based on their partitions. - show_pg_state (bool): If True, display the names of nodes in the preference graph; otherwise, use node IDs. - engine (str): The drawing engine to use for rendering (default is “dot”).

Returns:

A tuple containing two images as base64 encoded strings (semi-automaton and preference graph).

Return type:

tuple

prefltlf2pdfa.viz.paut2png(dot_semi_aut, dot_pref_graph, fpath='', fname='out')[source]

Save the semi-automaton and preference graph as PNG images.

Parameters:

  • dot_semi_aut (AGraph) – The DOT representation of the semi-automaton.

  • dot_pref_graph (AGraph) – The DOT representation of the preference graph.

  • fpath (str) – The file path where images should be saved.

  • fname (str) – The base name for the output files (without extension).

prefltlf2pdfa.viz.paut2svg(dot_semi_aut, dot_pref_graph, fpath='', fname='out')[source]

Save the semi-automaton and preference graph as SVG images.

Parameters:

  • dot_semi_aut (AGraph) – The DOT representation of the semi-automaton.

  • dot_pref_graph (AGraph) – The DOT representation of the preference graph.

  • fpath (str) – The file path where images should be saved.

  • fname (str) – The base name for the output files (without extension).

Module contents