navigation
search
Differences
This shows you the differences between two versions of the page.
|
vv-lab:guided-test-visualization [2015/02/18 22:37] egm created |
vv-lab:guided-test-visualization [2015/02/18 22:38] (current) egm [Visualization Output Format] |
||
|---|---|---|---|
| Line 23: | Line 23: | ||
| ==Visualization Output Format== | ==Visualization Output Format== | ||
| - | Runtime information is currently output into an XML file. See the [[XML Output DTD]]. | + | <code xml> |
| + | <!-- | ||
| + | JPF Guided Search Visualization DTD | ||
| + | A document type definition for the visualization XML generated by the JPF guided test | ||
| + | |||
| + | Contributors: Saint Wesonga <developer@swesonga.org> | ||
| + | Steven Morley <morleys2@byu.net> | ||
| + | |||
| + | Date: 2010/07/07 | ||
| + | |||
| + | --> | ||
| + | |||
| + | <!ENTITY % Number "CDATA"> | ||
| + | <!-- one or more digits --> | ||
| + | |||
| + | <!ELEMENT graph (node|edge|subgraph|jpfstate|jpfedge)*> | ||
| + | <!ELEMENT jpfstate (node|edge|jpfstate)*> | ||
| + | <!ELEMENT subgraph (node|edge)*> | ||
| + | <!ELEMENT jpfedge EMPTY> | ||
| + | <!ELEMENT edge EMPTY> | ||
| + | <!ELEMENT node (variables*)> | ||
| + | <!ELEMENT variables (variable+)> | ||
| + | <!ELEMENT variable EMPTY> | ||
| + | |||
| + | <!ATTLIST graph | ||
| + | id ID #IMPLIED> | ||
| + | |||
| + | <!ATTLIST jpfstate | ||
| + | id ID #IMPLIED> | ||
| + | |||
| + | <!ATTLIST subgraph | ||
| + | id ID #IMPLIED | ||
| + | label CDATA #IMPLIED> | ||
| + | |||
| + | <!ATTLIST variable | ||
| + | name CDATA #REQUIRED | ||
| + | type CDATA #IMPLIED | ||
| + | value CDATA #IMPLIED> | ||
| + | |||
| + | <!ATTLIST jpfedge | ||
| + | srcnode IDREF #REQUIRED | ||
| + | dstnode IDREF #REQUIRED> | ||
| + | |||
| + | <!ATTLIST edge | ||
| + | srcnode IDREF #REQUIRED | ||
| + | dstnode IDREF #REQUIRED> | ||
| + | |||
| + | <!ATTLIST node | ||
| + | id ID #REQUIRED | ||
| + | class CDATA #REQUIRED | ||
| + | method CDATA #REQUIRED | ||
| + | sourcecode CDATA #REQUIRED | ||
| + | sourceline %Number; #REQUIRED | ||
| + | srcpath CDATA #IMPLIED | ||
| + | bytepath CDATA #IMPLIED | ||
| + | bytecode CDATA #REQUIRED | ||
| + | bytecodeline %Number; #REQUIRED | ||
| + | executed (true|false) #REQUIRED | ||
| + | type (conditionalbranch|callsite|synchpoint|startsite|regularstmt) #REQUIRED | ||
| + | branchvalue (true|false) #IMPLIED | ||
| + | threadnumber %Number; "-1"> | ||
| + | </code> | ||
