Dafny: cannot generate model file

Apr 19, 2012 at 2:35 PM

I tried the command: dafny -mv:foo.model foo.dfy

It is supposed to generate a model file. But I could not find it.

Does the BVD still work?

Thanks!

Coordinator
Apr 21, 2012 at 12:02 AM

You seem to be using the command-line switch correctly.  If you're not getting the foo.model file, it's probably because your program has no errors.  Models are generated only for error messages.

Once you get the .model file, you should be able to invoke BVD on it.

  Rustan

Apr 24, 2012 at 2:00 PM

Hey Rustan,

That works. Thank you very much.

 

Yuyan

Apr 24, 2012 at 6:37 PM

I generated the model file from the following dafny code:

class ListNode {

  var data: int;

var next: ListNode;

}
static method Insert(hd: ListNode, n: ListNode)

requires hd != null && n != null;

modifies hd, n;

ensures n. next == old(hd.next);

{

n.next := hd.next;

hd.next := n;

}

However, when I tried to run BVD using the command: bvd foo.model, an error that Input string was not in a correct format was hit.

 

I could open the model file by starting BVD and trigger "Open model file ..." in the menu. But the Previous states are always empty.

Apr 24, 2012 at 8:29 PM

Previous states appear. Is it OK to trigger BVD not from command line?

Coordinator
Apr 25, 2012 at 6:57 PM

Odd, it seems to work for me.  I copied your program above into a file yuyan.dfy.  I then run:

    dafny yuyan.dfy /mv:foo.model

from the command line.  This produces an error message and generates the file foo.model.  I then run:

    bvd foo.model

which brings up the Boogie Verification Debugger, showing three states (<initial> and the states on lines 10 and 11).  I see two variables, displayed with the names hd#0 and n#1.  I can expand these nodes and click on any of the states.

I'm using Z3 version 3.2.  Is that what you have too?  (You can tell which version Boogie picking up by supplying the /trace flag to Boogie.)  If there was something wrong between Z3 and Boogie, I would have expected an error when running Boogie.  But you're getting the Input error when you run bvd, right?  I presume you're running the latest version of Boogie and bvd?



I would enclose foo.model, so you could try running it with bvd, but I don't see any button for me to include an attachment to this message.  So, I'll just include the contents of my foo.model below (sorry for the clutter).

*** MODEL
%lbl%+5746 -> true
%lbl%+10873 -> true
$InMethodContext -> true
$$Language$Dafny -> true
%lbl%@11147 -> false
class._System.int -> *2
lambda@1 -> *3
$_Frame@0@@0 -> *3
$rhs#0@0 -> *4
null -> *4
class._System.multiset -> *5
hd#0@@0 -> *6
n#1@@0 -> *6
TickTypeType -> *7
$Heap@1 -> *8
class._System.array -> *9
class._System.set -> *10
TType -> *11
refType -> *12
alloc -> *13
class._default._default -> *14
class._System.bool -> *15
$_Frame@0 -> *16
@MV_state_const -> 5
hd#0 -> *18
class._System.seq -> *19
ClassNameType -> *20
DatatypeTypeType -> *21
intType -> *22
_default.ListNode.data -> *23
lambda@0 -> *24
$ModuleContextHeight -> 0
$Heap@0 -> *26
_default.ListNode.next -> *27
BoxTypeType -> *28
$Heap@0@@0 -> *29
boolType -> *30
$Heap -> *31
class._default.ListNode -> *32
class._System.object -> *33
n#1 -> *34
$Tick -> **$Tick
$_Frame -> **$_Frame
$rhs#0 -> **$rhs#0
$rhs#1 -> **$rhs#1
FieldTypeInv0 -> {
  *35 -> *30
  *36 -> *22
  *37 -> *12
  else -> *30
}
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
type -> {
  *2 -> *20
  *15 -> *20
  *10 -> *20
  *19 -> *20
  *5 -> *20
  *9 -> *20
  *13 -> *35
  *33 -> *20
  *32 -> *20
  *23 -> *36
  *27 -> *37
  *14 -> *20
  *18 -> *12
  *34 -> *12
  *26 -> *38
  *31 -> *38
  *16 -> *39
  *24 -> *39
  false -> *30
  true -> *30
  *42 -> *28
  *43 -> *28
  *3 -> *39
  *6 -> *12
  *4 -> *12
  *29 -> *38
  *8 -> *38
  else -> *20
}
bool_2_U -> {
  false -> false
  true -> true
  else -> false
}
MapType2Type -> {
  *12 *30 -> *39
  else -> *39
}
$Box -> {
  false -> *42
  true -> *43
  else -> *42
}
FDim -> {
  *13 -> 0
  *23 -> 0
  *27 -> 0
  else -> 0
}
[3] -> {
  *31 *6 *13 -> true
  *31 *6 *27 -> *4
  *8 *6 *27 -> *6
  *29 *6 *27 -> *4
  *29 *6 *13 -> true
  *8 *6 *13 -> true
  *3 *6 *27 -> true
  else -> true
}
[4:=] -> {
  *31 *6 *27 *4 -> *29
  *29 *6 *27 *6 -> *8
  else -> *29
}
$Unbox -> {
  *30 *42 -> false
  *30 *43 -> true
  else -> false
}
U_2_bool -> {
  false -> false
  true -> true
  else -> false
}
MapType1Type -> {
  *12 -> *38
  else -> *38
}
@MV_state -> {
  5 0 -> true
  5 1 -> true
  else -> true
}
Ctor -> {
  *22 -> 0
  *30 -> 1
  *20 -> 2
  *12 -> 4
  *7 -> 6
  *28 -> 9
  *21 -> 10
  *11 -> 11
  *35 -> 3
  *36 -> 3
  *37 -> 3
  *38 -> 8
  *39 -> 12
  else -> 3
}
DeclType -> {
  *23 -> *32
  *27 -> *32
  else -> *32
}
MapType1TypeInv0 -> {
  *38 -> *12
  else -> *12
}
MapType2TypeInv0 -> {
  *39 -> *12
  else -> *12
}
$IsGoodHeap -> {
  *31 -> true
  *29 -> true
  *8 -> true
  else -> true
}
$HeapSucc -> {
  *31 *29 -> true
  *29 *8 -> true
  *31 *8 -> true
  else -> true
}
FieldType -> {
  *30 -> *35
  *22 -> *36
  *12 -> *37
  else -> *35
}
$IsCanonicalBoolBox -> {
  *42 -> true
  *43 -> true
  else -> true
}
MapType2TypeInv1 -> {
  *39 -> *30
  else -> *30
}
dtype -> {
  *6 -> *32
  else -> *32
}
*** STATE <initial>
  $Heap -> *31
  $Tick -> **$Tick
  hd#0 -> *6
  n#1 -> *6
  $_Frame -> **$_Frame
  $rhs#0 -> **$rhs#0
  $rhs#1 -> **$rhs#1
*** END_STATE
*** STATE yuyan.dfy(10,9)
  $Heap -> *29
  $_Frame -> *3
  $rhs#0 -> *4
*** END_STATE
*** STATE yuyan.dfy(11,10)
  $Heap -> *8
  $rhs#1 -> *6
*** END_STATE
*** END_MODEL

Apr 25, 2012 at 7:37 PM

My Z3 is 3.2 and boogie version is 2.2.30705.1126, which source is boogie-4b0b35f65c30.

And the windiff shows that  the model you posted and the model I generated with  version 2.2.30705.1126 are the same.

I got the same error when trying to trigger the BVD from command line with your model.

It works fine on the latest source boogie_afa038a2d4e8, which also shows the version  2.2.30705.1126.

I will use the latest boogie source to generate BVD. 

Thank you very much.