K-user mailing list

[Sergio Maffeis <maffeis AT doc.ic.ac.uk>]

Hi,

if i write a simple string in the stdout stream, my k program will run 
correctly but crash the model checker. here's a minimalist example:

1. the file doh.k is my language definition, that just prints what 
follows the keyword doh. i compile it with 'kompile doh.k 
--transition="kripke"'

2. the file a.doh is an example that prints "duff". i run it with
'krun a.doh' and it works fine

3. the file maudeoutput.xml is what i get after running 'krun a.doh 
--ltlmc "TrueLtl"' and the error message is "[Error] Critical: Cannot 
parse result xml from maude. If you believe this to be in error, please 
file a bug and attach .k/krun/maudeoutput.xml"

please can somebody help, i'm totally stuck here.

Sergio



require "builtins/model-checker.k"

module DOH
        imports LTL-HOOKS
        imports MODEL-CHECKER-HOOKS

configuration <T>
                <k> $PGM:K </k>
                <moe stream="stdout"> .List </moe>
              </T>

syntax K ::= LtlFormula
syntax K ::= "doh" String

rule <k> doh S:String => .K ... </k>
     <moe> ... . => ListItem(S) </moe>

endmodule

doh "duff"
<?xml version="1.0" encoding="US-ASCII" standalone="yes"?>
<maudeml>
 <reduce module="MCK">
  <term op="_`(_`)" kind="[KList,#LtlFormula]">
   <term op="'modelCheck`(_`,_`)" kind="[KLabel]"/>
   <term op="_`,`,_" kind="[KList,#LtlFormula]">
    <term op="_`(_`)" kind="[KList,#LtlFormula]">
     <term op="Bag2KLabel_" kind="[KLabel]">
      <term op="#initConfig" kind="[#ModelCheckerState]"/>
     </term>
     <term op=".KList" kind="[KList,#LtlFormula]"/>
    </term>
    <term op="_`(_`)" kind="[KList,#LtlFormula]">
     <term op="#_" kind="[KLabel]">
      <term op="TrueLtl" kind="[KList,#LtlFormula]"/>
     </term>
     <term op=".KList" kind="[KList,#LtlFormula]"/>
    </term>
   </term>
  </term>
 </reduce>
 <result total-rewrites="71" real-time-ms="0" cpu-time-ms="0" rewrites-per-second="266917">
  <term op="_`(_`)" sort="[KList,#LtlFormula]">
   <term op="'modelCheck`(_`,_`)" sort="KLabel"/>
   <term op="_`,`,_" sort="[KList,#LtlFormula]">
    <term op="_`(_`)" sort="[KList,#LtlFormula]">
     <term op="Bag2KLabel_" sort="[KLabel]">
      <term op="&lt;_>_&lt;/_>" sort="[#ModelCheckerState]">
       <term op="generatedTop" sort="CellLabel"/>
       <term op="&lt;_>_&lt;/_>" sort="[#ModelCheckerState]">
        <term op="T" sort="CellLabel"/>
        <term op="__" sort="[#ModelCheckerState]">
         <term op="&lt;_>_&lt;/_>" sort="BagItem">
          <term op="k" sort="CellLabel"/>
          <term op=".K" sort="K"/>
          <term op="k" sort="CellLabel"/>
         </term>
         <term op="&lt;_>_&lt;/_>" sort="[#ModelCheckerState]">
          <term op="moe" sort="CellLabel"/>
          <term op="__" sort="[List]">
           <term op="#ostream`(_`)" sort="List">
            <term op="_`(_`)" sort="KItem">
             <term op="#_" sort="KLabel">
              <term op="sNat_" number="1" sort="#NzNat">
               <term op="0" sort="#Zero"/>
              </term>
             </term>
             <term op=".KList" sort="KList"/>
            </term>
           </term>
           <term op="ListItem" sort="[List]">
            <term op="_`(_`)" sort="[KList,#LtlFormula]">
             <term op="String2DotK" sort="KLabel"/>
             <term op="_`(_`)" sort="[KList,#LtlFormula]">
              <term op="#checkTCPAnswer" sort="KLabel"/>
              <term op="_`(_`)" sort="[KList,#LtlFormula]">
               <term op="#_" sort="[KLabel]">
                <term op="#checkResult" sort="[#String]">
                 <term op="#containedRequest" sort="[#String]">
                  <term op="_#Socket_" sort="#Socket-Configuration">
                   <term op="#toSend" sort="#Socket-Msg">
                    <term op="&quot;1\00118\001writebytes\0011\001duff\001&quot;" sort="#String"/>
                   </term>
                   <term op="#start" sort="#Socket-Configuration">
                    <term op="sNat_" number="1" sort="#NzNat">
                     <term op="0" sort="#Zero"/>
                    </term>
                   </term>
                  </term>
                 </term>
                </term>
               </term>
               <term op=".KList" sort="KList"/>
              </term>
             </term>
            </term>
           </term>
           <term op="#removeCharsUponAck`(_`)" sort="List">
            <term op="_`(_`)" sort="KItem">
             <term op="#_" sort="KLabel">
              <term op="sNat_" number="4" sort="#NzNat">
               <term op="0" sort="#Zero"/>
              </term>
             </term>
             <term op=".KList" sort="KList"/>
            </term>
           </term>
           <term op="#buffer`(_`)" sort="List">
            <term op="_`(_`)" sort="KItem">
             <term op="#_" sort="KLabel">
              <term op="&quot;duff&quot;" sort="#String"/>
             </term>
             <term op=".KList" sort="KList"/>
            </term>
           </term>
          </term>
          <term op="moe" sort="CellLabel"/>
         </term>
        </term>
        <term op="T" sort="CellLabel"/>
       </term>
       <term op="generatedTop" sort="CellLabel"/>
      </term>
     </term>
     <term op=".KList" sort="KList"/>
    </term>
    <term op="TrueLtl" sort="#LtlFormula"/>
   </term>
  </term>
 </result>
</maudeml>