PyUPPAAL Documentation

PyUPPAAL Documentation

• Introduction
• Quickstart
  • 1. Installation
  • 2. Before Coding
  • 3. Load, Edit, and Verify a Model
  • 4. Find all patterns
  • 4. Verify with Multi-threads
  • 5. Get Communication Graph
  • 6. Backup of old docs
• Demo1 - PipeNet
  • 1. Problem Description
  • 2. Modeling the PipeNet
  • 3. Load the Model and Set Inputs & Observations
  • 4. Visualize the Architecture
  • 5. Find all patterns
• Demo2 - Pedestrian
  • 1. Problem Description
  • 2. Construct Model, and Verify with UPPAAL Solely
  • 3. find_all_patterns results
  • 4. Communication Graph
• Demo3 - Fault Diagnosis and Identification
  • 1. Fault Identification
  • 2. Fault Diagnosability
• Demo4 - Scripted Model Construction
  • 1. Setup Pyuppaal
  • 2. Create New Model File with declaration.
  • 3. Construct Receiver Template
  • 4. Construct Sender Template
  • 5. Set System and Queries
  • 6. Verify and Easy Verify
  • 7. Check Correctness
• Demo5 - Trace Parser
  • 1. Load the model, and get communication graph
  • 2. Construct the Input and Observation events
  • 3. Sey queries and Verify the model
  • 5. Analyze path conduction info
  • 4. Analyze node refractory info
• User API
  • pyuppaal.umodel
    • UModel
      • UModel.declaration
      • UModel.templates
      • UModel.system
      • UModel.queries
      • UModel.Element
      • UModel.ElementTree
      • UModel.model_path
      • UModel.max_location_id
      • UModel.broadcast_chan
      • UModel.xml
      • UModel.new()
      • UModel.write_xml_tree()
      • UModel.save_as()
      • UModel.save()
      • UModel.copy_as()
      • UModel.verify()
      • UModel.easy_verify()
      • UModel.get_communication_graph()
      • UModel.remove_template()
      • UModel.add_observer_monitor()
      • UModel.add_input_monitor()
      • UModel.add_template()
      • UModel.add_template_to_system()
      • UModel.find_a_pattern()
      • UModel.find_all_patterns()
      • UModel.find_all_patterns_iter()
      • UModel.fault_diagnosability()
      • UModel.fault_diagnosability_optimized()
      • UModel.fault_identification()
      • UModel.fault_tolerance()
      • UModel.load_xtr_trace()
  • pyuppaal.nta
    • Location
      • Location.Element
      • Location.xml
      • Location.from_xml()
    • Edge
      • Edge.Element
      • Edge.xml
      • Edge.from_xml()
    • Template
      • Template.Element
      • Template.xml
      • Template.from_xml()
  • pyuppaal.tracer
    • SimTrace
      • SimTrace.raw
      • SimTrace.states
      • SimTrace.clock_constraints
      • SimTrace.transitions
      • SimTrace.actions
      • SimTrace.untime_pattern
      • SimTrace.global_variables
      • SimTrace.filter_by_actions()
      • SimTrace.save_raw()
      • SimTrace.save()
      • SimTrace.trim_transitions()
    • OneClockZone
      • OneClockZone.clock1
      • OneClockZone.clock2
      • OneClockZone.is_equal
      • OneClockZone.bound_value
    • ClockZone
      • ClockZone.clockzones
    • Edges
      • Edges.start_location
      • Edges.end_location
      • Edges.guard
      • Edges.has_guard
      • Edges.sync
      • Edges.update
      • Edges.process
      • Edges.is_sync
      • Edges.sync_type
      • Edges.sync_symbol
    • Transition
      • Transition.sync
      • Transition.start_process
      • Transition.end_process
      • Transition.edges
      • Transition.action
    • GlobalVar
• ALL API
  • pyuppaal.pyuppaal
    • set_verifyta_path()
    • DeveloperTools
      • DeveloperTools.get_verifyta_path_dev()
      • DeveloperTools.set_verifyta_path_dev()
  • pyuppaal.umodel
    • UModel
      • UModel.declaration
      • UModel.templates
      • UModel.system
      • UModel.queries
      • UModel.Element
      • UModel.ElementTree
      • UModel.model_path
      • UModel.max_location_id
      • UModel.broadcast_chan
      • UModel.xml
      • UModel.new()
      • UModel.write_xml_tree()
      • UModel.save_as()
      • UModel.save()
      • UModel.copy_as()
      • UModel.verify()
      • UModel.easy_verify()
      • UModel.get_communication_graph()
      • UModel.remove_template()
      • UModel.add_observer_monitor()
      • UModel.add_input_monitor()
      • UModel.add_template()
      • UModel.add_template_to_system()
      • UModel.find_a_pattern()
      • UModel.find_all_patterns()
      • UModel.find_all_patterns_iter()
      • UModel.fault_diagnosability()
      • UModel.fault_diagnosability_optimized()
      • UModel.fault_identification()
      • UModel.fault_tolerance()
      • UModel.load_xtr_trace()
  • pyuppaal.monitors
    • Monitors
      • Monitors.fault_monitor()
      • Monitors.observer_suffix_monitor()
      • Monitors.obs_after_fault_monitor()
      • Monitors.input_after_fault_monitor()
      • Monitors.tolerance_checker_monitor()
      • Monitors.input_template()
      • Monitors.observer_template()
  • pyuppaal.verifyta
    • Verifyta
      • Verifyta.verifyta_path
      • Verifyta.get_env()
      • Verifyta.get_uppaal_version()
      • Verifyta.set_verifyta_path()
      • Verifyta.cmd()
      • Verifyta.compile_to_if()
      • Verifyta.verify()
  • pyuppaal.tracer
    • SimTrace
      • SimTrace.raw
      • SimTrace.states
      • SimTrace.clock_constraints
      • SimTrace.transitions
      • SimTrace.actions
      • SimTrace.untime_pattern
      • SimTrace.global_variables
      • SimTrace.filter_by_actions()
      • SimTrace.save_raw()
      • SimTrace.save()
      • SimTrace.trim_transitions()
    • OneClockZone
      • OneClockZone.clock1
      • OneClockZone.clock2
      • OneClockZone.is_equal
      • OneClockZone.bound_value
    • ClockZone
      • ClockZone.clockzones
    • Edges
      • Edges.start_location
      • Edges.end_location
      • Edges.guard
      • Edges.has_guard
      • Edges.sync
      • Edges.update
      • Edges.process
      • Edges.is_sync
      • Edges.sync_type
      • Edges.sync_symbol
    • Transition
      • Transition.sync
      • Transition.start_process
      • Transition.end_process
      • Transition.edges
      • Transition.action
    • GlobalVar
  • pyuppaal.nta
    • Location
      • Location.Element
      • Location.xml
      • Location.from_xml()
    • Edge
      • Edge.Element
      • Edge.xml
      • Edge.from_xml()
    • Template
      • Template.Element
      • Template.xml
      • Template.from_xml()
  • pyuppaal.build_cg
    • Mermaid
      • Mermaid.mermaid_str
      • Mermaid.mermaid_list
      • Mermaid.beautify()
      • Mermaid.remove()
      • Mermaid.export()
    • get_str_before()
    • get_str_after()
    • Node
    • XmlTemplate
      • XmlTemplate.init_name()
      • XmlTemplate.get_all_sync()
      • XmlTemplate.get_param()
      • XmlTemplate.get_instance()
    • XmlReader
      • XmlReader.init_template()
      • XmlReader.get_notes()
    • add_edge()
    • build_cg_code()
    • build_cg()

Indices and tables

• Index

• Module Index

• Search Page