• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
        • Vwsim-users-guide
          • Vwsim-tutorial
          • Vwsim-output
            • Vwsim-output-request-format
          • Vwsim-input
          • Vwsim-build-and-setup
          • Vwsim-commands
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Vwsim-users-guide

Vwsim-output

VWSIM output formats.

Output

VWSIM saves all values produced during a simulation; these values may be used for subsequent processing such a analysis and/or printing. The saved results can be processed in the following ways (see below). An advanced user of VWSIM can access the entire trace of simulation values and write programs to explore the data and even control the simulation as it advances; this advanced mechanism is not documented presently (within this collection of notes), but can be explored by consulting the VWSIM source code.

A VWSIM user interacts with VWSIM through a (Lisp-style) command-line, read-eval-print loop. Commands can be given to request the various output.

    Comma-Separated Values (CSV) file

    The user-requested values are written to a file in CSV format.

    Association-list

    The user-requested values are returned in a LISP-style association (key-value pair) list. The values can be accessed interactively by name using assoc-equal.

    Saved (LISP) file

    An entire simulation state is saved to a file, which can be provided to VWSIM at a later time so as to resume the saved simulation.

    Graphical Plots

    The user-requested values can be plotted directly from the ACL2 loop using gnuplot.

Subtopics

Vwsim-output-request-format
How to format output requests from a VWSIM simulation.