如何保存Uppaal建模过程中产生的变量值？

Hey Josi, I've run into this exact issue before—getting those time-varying integer variables out of Uppaal can feel tricky at first, but there are a few solid ways to make it happen. Let's break down the solutions that work:

1. Use Uppaal's Built-in Simulator Export (Easiest for Manual Work) #

You don't need to mess with APIs for basic use cases! The Uppaal simulator has a built-in option to export traces including variable values:

• Run your simulation and generate a trace in the simulator view.
• Right-click on the trace and select Export Trace....
• In the export dialog:
  • Pick either XML or Text as your output format.
  • Look for a checkbox like "Include variable values" (labeling might vary slightly by version) and make sure it's checked.
• Once exported, your XML file will have <variable> nodes under each state entry, and the text file will list each timestamp alongside the current value of every tracked variable.

2. Extend the Uppaal Java API to Capture Variables #

If you need to automate this via code, the Java API does support accessing variable values—you just need to dig a bit deeper into the State objects:
Here's a quick snippet to modify your existing code to log variables:

// Assume you've already fetched a trace object from the API
for (Transition transition : trace) {
    // Capture variables from the source state (before the transition)
    State sourceState = transition.getSource();
    Map<String, Value> sourceVars = sourceState.getVariables();
    
    // Log time and variable values (write to file instead of print if needed)
    System.out.printf("Timestamp: %.2f%n", sourceState.getTime());
    for (Map.Entry<String, Value> varEntry : sourceVars.entrySet()) {
        System.out.printf("  %s = %s%n", varEntry.getKey(), varEntry.getValue());
    }

    // Optional: Capture variables from the target state (after the transition)
    State targetState = transition.getTarget();
    // ... repeat the same logic for targetState.getVariables()
}

You can redirect this output to a text file, or build an XML structure programmatically to save variable states in that format.

3. Automate with the verifyta Command-Line Tool #

For batch processing or integration with scripts, the verifyta tool (included with Uppaal) is perfect. You can run queries and export traces with variable data directly to XML:

• Create a query file (e.g., my_query.q) with a trace-generating query like:

  E<> true  // Generates a full execution trace
  

• Run this command in your terminal:

  verifyta -t 1 -x output_variables.xml your_model.xml my_query.q
  

  • -t 1 tells verifyta to export the trace
  • -x specifies XML output
    The resulting XML will include all variable values at each state in the trace.

Quick Notes #

• Double-check your Uppaal version: Some older releases might have slightly different menu options or API method names, but the core functionality exists across recent versions.
• For text files, the simulator's export will give you a human-readable format, while the API/verifyta let you customize the structure to fit your needs.

内容的提问来源于stack exchange，提问作者Josi