why3session.dtd 1.93 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
<!ELEMENT why3session (prover*, file*)>
MARCHE Claude's avatar
MARCHE Claude committed
2
<!ATTLIST why3session shape_version CDATA #IMPLIED>
3

MARCHE Claude's avatar
MARCHE Claude committed
4 5 6 7
<!ELEMENT prover EMPTY>
<!ATTLIST prover id CDATA #REQUIRED>
<!ATTLIST prover name CDATA #REQUIRED>
<!ATTLIST prover version CDATA #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
8
<!ATTLIST prover alternative CDATA #IMPLIED>
9 10
<!ATTLIST prover timelimit CDATA #IMPLIED>
<!ATTLIST prover memlimit CDATA #IMPLIED>
11
<!ATTLIST prover steplimit CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
12

13
<!ELEMENT file (path*, theory*)>
14
<!ATTLIST file name CDATA #IMPLIED>
15
<!ATTLIST file verified CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
16
<!ATTLIST file proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
17

18 19 20
<!ELEMENT path EMPTY>
<!ATTLIST path name CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
21
<!ELEMENT theory (label*,goal*)>
MARCHE Claude's avatar
MARCHE Claude committed
22
<!ATTLIST theory name CDATA #REQUIRED>
23
<!ATTLIST theory verified CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
24
<!ATTLIST theory proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
25

MARCHE Claude's avatar
MARCHE Claude committed
26
<!ELEMENT goal (label*, proof*, transf*)>
MARCHE Claude's avatar
MARCHE Claude committed
27 28
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
29
<!ATTLIST goal sum CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
30
<!ATTLIST goal shape CDATA #IMPLIED>
31
<!ATTLIST goal proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
32

33
<!ELEMENT proof (result|undone|internalfailure|unedited)>
MARCHE Claude's avatar
MARCHE Claude committed
34
<!ATTLIST proof prover CDATA #REQUIRED>
35 36
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
37
<!ATTLIST proof steplimit CDATA #IMPLIED>
38 39
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
40 41

<!ELEMENT result EMPTY>
42
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|steplimitexceeded|failure|highfailure) #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
43
<!ATTLIST result time CDATA #IMPLIED>
44
<!ATTLIST result steps CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
45

46
<!ELEMENT undone EMPTY>
47
<!ELEMENT unedited EMPTY>
48

49 50 51
<!ELEMENT internalfailure EMPTY>
<!ATTLIST internalfailure reason CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
52 53
<!ELEMENT transf (goal*)>
<!ATTLIST transf name CDATA #REQUIRED>
54
<!ATTLIST transf proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
55 56 57 58
<!ATTLIST transf arg1 CDATA #IMPLIED>
<!ATTLIST transf arg2 CDATA #IMPLIED>
<!ATTLIST transf arg3 CDATA #IMPLIED>
<!ATTLIST transf arg4 CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61

<!ELEMENT label EMPTY>
<!ATTLIST label name CDATA #REQUIRED>