PReach / User.Manual

   1
   2
   3
   4
   5
   6
   7
   8
   9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
  21
  22
  23
  24
  25
  26
  27
  28
  29
  30
  31
  32
  33
  34
  35
  36
  37
  38
  39
  40
  41
  42
  43
  44
  45
  46
  47
  48
  49
  50
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124
 125
 126
 127
 128
 129
 130
 131
 132
 133
 134
 135
 136
 137
 138
 139
 140
 141
 142
 143
 144
 145
 146
 147
 148
 149
 150
 151
 152
 153
 154
 155
 156
 157
 158
 159
 160
 161
 162
 163
 164
 165
 166
 167
 168
 169
 170
 171
 172
 173
 174
 175
 176
 177
 178
 179
 180
 181
 182
 183
 184
 185
 186
 187
 188
 189
 190
 191
 192
 193
 194
 195
 196
 197
 198
 199
 200
 201
 202
 203
 204
 205
 206
 207
 208
 209
 210
 211
 212
 213
 214
 215
 216
 217
 218
 219
 220
 221
 222
 223
 224
 225
 226
 227
 228
 229
 230
 231
 232
 233
 234
 235
 236
 237
 238
 239
 240
 241
 242
 243
 244
 245
 246
 247
 248
 249
 250
 251
 252
 253
 254
 255
 256
 257
 258
 259
 260
 261
 262
 263
 264
 265
 266
 267
 268
 269
 270
 271
 272
 273
 274
 275
 276
 277
 278
 279
 280
 281
 282
 283
 284
 285
 286
 287
 288
 289
 290
 291
 292
 293
 294
 295
 296
 297
 298
 299
 300
 301
 302
 303
 304
 305
 306
 307
 308
 309
 310
 311
 312
 313
 314
 315
 316
 317
 318
 319
 320
 321
 322
 323
 324
 325
 326
 327
 328
 329
 330
 331
 332
 333
 334
 335
 336
 337
 338
 339
 340
 341
 342
 343
 344
 345
 346
 347
 348
 349
 350
 351
 352
 353
 354
 355
 356
 357
 358
 359
 360
 361
 362
 363
 364
 365
 366
 367
 368
 369
 370
 371
 372
 373
 374
 375
 376
 377
 378
 379
 380
 381
 382
 383
 384
 385
 386
 387
 388
 389
 390
 391
 392
 393
 394
 395
 396
 397
 398
 399
 400
 401
 402
 403
 404
 405
 406
 407
 408
 409
 410
 411
 412
 413
 414
 415
 416
 417
 418
 419
 420
 421
 422
 423
 424
 425
 426
 427
 428
 429
 430
 431
 432
 433
 434
 435
 436
 437
 438
 439
 440
 441
 442
 443
 444
 445
 446
 447
 448
 449
 450
 451
 452
 453
 454
 455
 456
 457
 458
 459
 460
 461
 462
 463
 464
 465
 466
 467
 468
 469
 470
 471
 472
 473
 474
 475
 476
 477
 478
 479
 480
 481
 482
 483
 484
 485
 486
 487
 488
 489
 490
 491
 492
 493
 494
 495
 496
 497
 498
 499
 500
 501
 502
 503
 504
 505
 506
 507
 508
 509
 510
 511
 512
 513
 514
 515
 516
 517
 518
 519
 520
 521
 522
 523
 524
 525
 526
 527
 528
 529
 530
 531
 532
 533
 534
 535
 536
 537
 538
 539
 540
 541
 542
 543
 544
 545
 546
 547
 548
 549
 550
 551
 552
 553
 554
 555
 556
 557
 558
 559
 560
 561
 562
 563
 564
 565
 566
 567
 568
 569
 570
 571
 572
 573
 574
 575
 576
 577
 578
 579
 580
 581
 582
 583
 584
 585
 586
 587
 588
 589
 590
 591
 592
 593
 594
 595
 596
 597
 598
 599
 600
 601
 602
 603
 604
 605
 606
 607
 608
 609
 610
 611
 612
 613
 614
 615
 616
 617
 618
 619
 620
 621
 622
 623
 624
 625
 626
 627
 628
 629
 630
 631
 632
 633
 634
 635
 636
 637
 638
 639
 640
 641
 642
 643
 644
 645
 646
 647
 648
 649
 650
 651
 652
 653
 654
 655
 656
 657
 658
 659
 660
 661
 662
 663
 664
 665
 666
 667
 668
 669
 670
 671
 672
 673
 674
 675
 676
 677
 678
 679
 680
 681
 682
 683
 684
 685
 686
 687
 688
 689
 690
 691
 692
 693
 694
 695
 696
 697
 698
 699
 700
 701
 702
 703
 704
 705
 706
 707
 708
 709
 710
 711
 712
 713
 714
 715
 716
 717
 718
 719
 720
 721
 722
 723
 724
 725
 726
 727
 728
 729
 730
 731
 732
 733
 734
 735
 736
 737
 738
 739
 740
 741
 742
 743
 744
 745
 746
 747
 748
 749
 750
 751
 752
 753
 754
 755
 756
 757
 758
 759
 760
 761
 762
 763
 764
 765
 766
 767
 768
 769
 770
 771
 772
 773
 774
 775
 776
 777
 778
 779
 780
 781
 782
 783
 784
 785
 786
 787
 788
 789
 790
 791
 792
 793
 794
 795
 796
 797
 798
 799
 800
 801
 802
 803
 804
 805
 806
 807
 808
 809
 810
 811
 812
 813
 814
 815
 816
 817
 818
 819
 820
 821
 822
 823
 824
 825
 826
 827
 828
 829
 830
 831
 832
 833
 834
 835
 836
 837
 838
 839
 840
 841
 842
 843
 844
 845
 846
 847
 848
 849
 850
 851
 852
 853
 854
 855
 856
 857
 858
 859
 860
 861
 862
 863
 864
 865
 866
 867
 868
 869
 870
 871
 872
 873
 874
 875
 876
 877
 878
 879
 880
 881
 882
 883
 884
 885
 886
 887
 888
 889
 890
 891
 892
 893
 894
 895
 896
 897
 898
 899
 900
 901
 902
 903
 904
 905
 906
 907
 908
 909
 910
 911
 912
 913
 914
 915
 916
 917
 918
 919
 920
 921
 922
 923
 924
 925
 926
 927
 928
 929
 930
 931
 932
 933
 934
 935
 936
 937
 938
 939
 940
 941
 942
 943
 944
 945
 946
 947
 948
 949
 950
 951
 952
 953
 954
 955
 956
 957
 958
 959
 960
 961
 962
 963
 964
 965
 966
 967
 968
 969
 970
 971
 972
 973
 974
 975
 976
 977
 978
 979
 980
 981
 982
 983
 984
 985
 986
 987
 988
 989
 990
 991
 992
 993
 994
 995
 996
 997
 998
 999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
NOTE: This is the User.Manual from the standard Murphi 3.1 distribution.
Most of it is relevant to PReach; to avoid confusion a few sections that 
are irrelevant to PReach have been deleted in this version.
(the deleted sections have still been left in the Contents, however)...



  		   Murphi Annotated Reference Manual

	                       Release 3.1

  	  	       Ralph Melton, David L. Dill
	 	 Updated by C. Norris Ip and Ulrich Stern
			        July 1996


Contents:
1.  Introduction
    1.1  Whence "Murphi"?
    1.2  Evolution of Murphi

2.  Overview of Murphi 
    2.1 Structure of a Murphi Description
    2.2 Four simple steps to use Murphi to verify a system
    2.3 Murphi Execution Model
    2.4 Options of the Murphi Compiler
    2.5 Using the Generated Special Purpose Verifier

3.  Basic Concepts
    3.1  BNF
    3.2  Lexical Conventions
    3.3  Program Structure

4.  Declarations
    4.1  Constant, type, and variable declarations.
    4.2  Procedure and Function declarations.

5.  Expressions

6.  Statements

7.  Rules, Startstates, and Invariants

8.  Reduction Techniques
    8.1 Symmetry and Multiset Reduction
    8.2 Hash Compaction

A.  Symmetry Reduction

B.  Multiset Reduction


1.  INTRODUCTION

The Murphi description language is a high-level description language
for finite-state asynchronous concurrent systems.  Murphi is
high-level in the sense that many features found in common high-level
programming languages such as Pascal or C are part of Murphi.  For
example, Murphi has user-defined data types, procedures, and
parameterization of descriptions.


2. Overview of Murphi

2.1 Structure of a Murphi Description:

A Murphi description consists of declarations of constants, types,
global variables, and procedures; a collection of transition rules; a
description of the initial states; and a set of invariants.

The behavioral part of Murphi is a collection of transition rules.
Each transition rule is an guarded command consists of a condition (a
Boolean expression on the global variables) and an action (a statement
that can modify the values of the variables).

The condition and the action are both written in a Pascal-like
language.  The action can be an arbitrarily complex statement
containing loops and conditionals.  No matter how complex it is, the
action is executed ATOMICALLY -- no other rule can change the
variables or otherwise interfere with it while it is being executed.

2.3 Murphi Execution Model:

A Murphi state is an assignment of values to all of the global
variables of the description.  

An execution of the description can be generated by cycling infinitely
through the following:

Repeat forever:

    a) Find all rules whose conditions are true in the current state.
       (i.e. conditional expressions are true, given the current values
       of the global variables).

    b) Choose one arbitrarily and execute the action, yielding a new
       state.

Note that Murphi descriptions are nondeterministic, because of the
arbitrary choice in step b.  The user has no control over how this
choice is made, so a "correct" Murphi program must do the right thing
no matter which rules are chosen.  However, once a rule has been
chosen, the action is deterministic (there is a unique next state).

This execution model is good for describing asynchronous systems
(where different processes run at arbitrary speed) which interact
via shared variables (process A affects process B by writing to
a variable the process B reads).  Message passing can be modelled
by reading from and writing to a buffer variable or array.

As states are generated by the verifier, various conditions are
checked.  There can be run-time errors of various kinds, most notably
out-of-bounds errors on assignments or array indexing.  There is are
explicit "assert" and "error" statement that can be called within an
action.  If one of these conditions occurs, the verifier halts and
prints a diagnostic consisting of a reconstructed sequence of states
that leads from the initial state to the error state.  The verifier
also does this if one of the invariant expressions (given by the
user as part of the description) is false for the current state,
or if the current state is a "deadlock state" (has no successor
states except itself).


3.  BASIC CONCEPTS

3.1  Backus-Naur Form (BNF)

The syntax is specified in this manual in a Backus-Naur Form:
    <> denote nonterminals;
    [] denote optional sections;
    {} denote repetition zero or more times.
    a | b denotes either a or b.
    () denote grouping.

When any of these symbols are required within the language, they
are escaped with backslashes.

3.2  Lexical Conventions

The following are reserved words in Murphi:              

    alias           array           assert          begin           
    boolean         by              case            clear
    const           do              else            elsif
    end             endalias        endexists       endfor
    endforall       endfunction     endif           endprocedure
    endrecord       endrule         endruleset      endstartstate
    endswitch       endwhile        enum            error
    exists          false           for             forall
    function        if              in              interleaved
    invariant       of              procedure       process
    program         put             record          return
    rule            ruleset         startstate      switch
    then            to              traceuntil      true
    type            var             while

Reserved words are written out in the BNF.
Some of these reserved words do not yet have defined meanings;
these are reserved for future expansion. Those words are
in, interleaved, process, program, traceuntil.

CASE-SENSITIVITY: Murphi is case-sensitive, except for the reserved
words.  'foo' and 'Foo' represent different identifiers.  'Begin' and
'BeGiN' represent the same keyword.

SYNONYM: The keyword 'end' is a synonym for every specific type of
end: 'end' may be used freely in place of 'endrule', 'endfor', 


IDENTIFIERS: An identifier is any sequence of letters, underscores,
and digits beginning with a letter.  All identifiers beginning with
underscore are reserved for use by the system.  Identifiers are
referred to in the BNF below as <ID>.

STRINGS: A string, referred to in the BNF as <string> is a sequence of
characters other than double quote (\") enclosed in double quotes.

INTEGER CONSTANTS: Integer constants, <integer-constant> in the BNF,
are specified in base 10.

Comments: There are two types of comments in Murphi: Ada-style
comments that begin with -- and end with a newline.  C-style comments
that begin with /* and end with */. C-style comments do not nest.

3.3  Program Structure

A Murphi program has the following structure, with comments about
each section set off by --:

<Program> ::= { <decl> }	-- Constant, type, and variable declarations
	      { <procdecl> }	-- Procedure and function declarations
	      { <rules> }	-- rules, startstates, and invariants

A Murphi program implicitly determines a state graph.  A state is an
assignment of a value to each global variable.  The start states of
the graph are defined by startstates in the <rules> section of the
program.  The next state relation of the graph is defined by rules
within the <rules> section of the program.


4. DECLARATIONS

4.1 Constant, type, and variable declarations

Declarations have the following syntax:

	<decl> ::=	const { <constdecl> ; }
		 |	type { <typedecl> ; }
		 |	var { <vardecl> ; }

Constant declarations:

	<constdecl> ::=	<ID> : <expr>

The <expr> of a constant declaration must have a value that can be
evaluated at compile time.

Type declarations:

	<typedecl> ::=	<ID> : <typeExpr>

The special enumerated type "boolean" is predefined, along with the
constants "true" and "false". The type integer is not predefined,
because using general integers without restricting them to subranges
would consume memory horribly.

The simple types are booleans, enumerations, finite subranges of
integers.

The compound types are arrays of compound or simple types,
records of compound or simple types.

The index types of arrays must be simple types.
	
	<typeExpr> ::=	<ID>		-- a previously defined type.
	<typeExpr> ::=	<expr> .. <expr>	-- Integer subrange.
	<typeExpr> ::=	enum \{ <ID> {, <ID> } \} -- enumeration.
	<typeExpr> ::=	record { <vardecl> } end
	<typeExpr> ::=	array \[ <typeExpr> \] of <typeExpr>

Variable declarations:

	<vardecl>  ::=	<ID> { , <ID> } : <typeExpr>


Example:  The following example illustrates declarations.

   const 
     I: 2;
     J: 31415 * I / 9;                 -- J will be 6981

   type
     val_t: 0..99;                     -- simple types.
     ind_t: 1..i;
     enum_t: enum { x, y, z };
     b: boolean;

     r_t: record f:0..1; g: 0..2; end; -- Record.
     rr_t: record r: r_t; s: r_t; end; -- Record of record.

     a_t: array [ ind_t ] of 19..29;   -- 1-dimensional array.
     aa_t: array [ ind_t ] of a_t;     -- 2-dimensional array.

     ar_t: array [ 1..2 ] of r_t;      -- Array of record.
     ra_t: record a1: a_t; foo: ind_t; end;     -- Record with array.

     ae_t: array [ enum_t ] of enum_t; -- Array with enum index and range.
     aae_t: array [ ind_t ] of ae_t;   -- 2-dim array, 2nd index is enum.
     re_t: record f: enum_t; end;      -- Record of enum.

   var
     val : val_t;
     arr : ae_t;
     rec : record foo: ind_t; bar: boolean; end;
    
    
4.2 Procedure and function declarations
    
All procedures and functions must be declared at the top level of the
program, with the following syntax:

	<procdecl> ::=	<procedure>
	             | 	<function>

	<procedure> ::=	procedure <ID> \( [ <formal> { ; <formal> } ] \) ;
			[ { <decl> } begin ] [ <stmts> ] end;

	<function> ::=	function <ID> \( [ <formal> { ; <formal> } ] \)
			: <typeExpr>; 
			[ { <decl> } begin ] [ <stmts> ] end;

Unlike Pascal procedures, procedures and functions with no arguments
still need the parentheses surrounding the empty parameter list.

Functions must return a value with a return statement (q.v.) at some
point in the function.  Functions can have side effects; however,
there are restrictions on the use of functions with side effects.

The format of the parameter list in a procedure or a function is:

	<formal> ::=	[var] <ID> { , <ID> } : <typeExpr>
	 
Formal parameters declared "var" are passed by reference.  Formals
that are not declared "var" are passed by reference, but the function
or procedure is not allowed to modify them.

Formal parameter declarations and local declarations shadow declarations
outside their scope.

Example:  the following example illustrates procedures.

	procedure Swap(var i, j: val_t);
	var temp: val_t;
	begin
	  temp := i;
	  i := j;
	  j := temp;
	end;
	
	function plustwo(input: val_t): val_t;
	const two : 2;
	begin
	  return (input + two);
	end;


5.  EXPRESSIONS

Type equivalence is by name.  Expressions of any integer subrange type
are legal wherever an integer expression is legal (although it may
generate a run-time error; see below about assignments).  Booleans
are not type-compatible with integer expressions.

It is an error to take the value of an variable that has not yet
been assigned a value.  This error is detected at run time.
(All run-time errors is detected by the verifier.)

It is an error to use an out-of-bounds index for an array.  This
too is detected at run time.

Designators:

	<designator> :=	<ID> { . <ID> | \[ <expr> \] }

As usual, the form <designator>.<ID> refers to selecting a field
of a record, and the form <designator> [<expr>] is for selecting
an element of an array.

Expressions:

<expr> :=  \( expr \)
	 | <designator>
	 | <integer-constant>
	 | <ID> \( <actuals> \)		-- a function call.
	 | forall <quantifier> 
	   do <expr> endforall		-- universal quantification.
	 | exists <quantifier>
	   do <expr> endexists		-- existential quantification.
	 | <expr> + <expr>
	 | <expr> - <expr>
	 | <expr> * <expr>		-- multiplication.
	 | <expr> / <expr>		-- integer division.
	 | <expr> % <expr>		-- remainder.
	 | ! <expr>			-- logical negation.
	 | <expr> | <expr>		-- logical disjunction.
	 | <expr> & <expr>		-- logical conjunction.
	 | <expr> -> <expr>		-- logical implication.
	 | <expr> < <expr>
	 | <expr> <= <expr>
	 | <expr> > <expr>
	 | <expr> >= <expr>
	 | <expr> = <expr>
	 | <expr> != <expr>
	 | <expr> ? <expr> : <expr>	-- C-style conditional expression.

Operators:

The priority of operators is as follows, with lowest-priority
operators first and operators on the same line having equal priority:

		?:			
		->			
		|			
 		&
		!
		< <= = != >= > 
		+ -
		* / %

  a) '+', '-', '*', '/', '%', '<', '<=', '>=', and '>' are only
     defined on integer operands.
  b) '=' and '!=' are only defined on simple operands.
  c) '!', '&', '!', and '->' are only defined on boolean operands.
  d) For the '?:' operator, the test must be a boolean expression, and
     the two alternatives must be of compatible type.
  e) '+', '-', '*', '/', and '*' return an integer, the rest return
      booleans, except for '?:'.

'Forall' and 'Exists' Operators:

See below, under the 'for' statement, for the specification of the
<quantifier> used in quantified expressions, i.e. exist's and
forall's.  For a quantified expression, the subexpression must
be a boolean expression; it is evaluated once for each value of
the quantifier.  A forall is true iff its expression is true
for every value of the quantifier; an exists is true if its
expression is true for some value of the quantifier.


6.  STATEMENTS.

The followings are the statements in Murphi:

	<stmts> ::= <stmt> {; [<stmt>] }
	
	<stmt> ::= <assignment>         /* assignment */
	         | <ifstmt>		/* if statement */
		 | <switchstmt>		/* switch statement */
		 | <forstmt>		/* for statement */
		 | <whilestmt>		/* while statement */
		 | <aliasstmt>		/* alias statement */
		 | <proccall>		/* procedure call */
		 | <clearstmt>		/* clear statement */
		 | <errorstmt>		/* error assertion */
		 | <assertstmt>		/* assertion */
		 | <putstmt>		/* output statement */
		 | <returnstmt>		/* function return */

Assignment:

	<assignment> ::= <designator> := <expression>

The target and the expression must have compatible types, and the
target must not be declared const.

It is an error to assign a value to a variable that is outside the
range for that variable.  This error is detected at run time.

If statement:

	<ifstmt> ::= if <expr> then [ <stmts> ]
		        { elsif <expr> then [ <stmts> ] }
			[ else [ <stmts> ] ]
		     endif

Each of the <expr>'s must be of boolean type.

Switch statement:

	<switchstmt> ::= switch <expr>
			   { case <expr> {, expr} : [ <stmts> ] }
			   [ else [ <stmts> ] ]
			 endswitch

Each of the expressions in the case must be a constant of a compatible
type with the switch expression.  If no case expression is matched,
the code labelled 'else' is executed.

There is no fall through on cases.

For statement:

	<forstmt> ::= for <quantifier> do [stmts] endfor

Quantifiers apply to for statements, to quantified expressions, and to
rulesets.

	<quantifier> ::= <ID> : <typeExpr>
		       | <ID> := <expr> to <expr> [ by <expr> ]

The first form executes the body of the for statement or evaluates the
body of the quantified expression, etc., for each value in the
<typeExpr> (which must be a simple type), from least to greatest
value.  The second form corresponds to the Modula-2 FOR statement.
The two expressions must be of integer type, and the by expression
must be a constant expression.

Using a quantifier, in a for statement or a quantified expression,
declares the <ID> of the quantifier local to the for statement,
shadowing any external declarations.  It is illegal to modify the
quantifier variable from within the body of the for loop.

While statement:

	<whilestmt> ::= while <expr> do [stmts] end

An infinite loop is a runtime error.  Although this is decidable
because a bound on the total number of states can be computed,
infinite loops obviously pose a practical problem for the verifier.
Right now, the verifier stops with an error message after 1000
iterations as an default option (which may be changed by changing a
constant in the file mu_prolog.inc).  The user may change this limit
by a command-line argument.

Alias statement:

	<aliasstmt> ::= alias <alias> { ; <alias> } do [ <stmts> ] end

	<alias> ::= <ID> : <expr>

	<ID>'s declared in aliases shadow external declarations of the same ID.

Aliases behave differently depending on whether the <expr> is or is
not an lvalue.  If the <expr> is an lvalue, then <ID> is defined as
the lvalue associated with that expression when the alias statement is
entered.  If <expr> is not an lvalue, then <ID> gets the value
associated with <expr> when the alias statement is entered, and <ID>
may not be changed within the alias block.

	Example:

	    -- i = 2 beforehand; arr[2] = 1.
	    alias
	      foo : arr[i] 	-- foo gets identified with arr[2]
	      bar : arr[i] + 1	-- bar gets identified with 2.
	    do
	      arr[i] := 3;	-- now, foo = 3, but bar = 2.
	      i := 1;		-- foo is still bound to a[2].
	      foo := 4;		-- arr[2] is now 4. bar = 2.
	      bar := 2;		-- Illegal.
	    end

Procedure call:

	<proccall> ::= <ID> \( <expr> {, <expr> } \)

This obeys all the standard rules of procedures.  Const formal
parameters can be passed an actual of any compatible type; var
parameters must be passed an lvalue of the same type; a var parameter
of a subrange type must be passed an lvalue of the same subrange type.

Clear statement:

	<clearstmt> ::= clear <designator>

This sets all components of an lvalue to the minimum values of their
type.  The minimum value of an enumerated type is considered to be the
first value declared in the list of names. The minimum value of the
type boolean is false.  

NOTE: Clear is frequently used to set "uninteresting" variables to a
fixed value; otherwise, many states would be created during
verification with random values in these variables.  Use of clear for
other purposes is not encouraged.  We are thinking about replacing
this with an "undefine" operator that assigns a reserved undefined
value, which would be safer.

Error assertion:

	<errorstmt> ::= error <string>

An error statement generates a run-time error.  In the verifier, if an
error statement is executed, verification terminates, the specified
string is printed, and a failure trace is printed if requested.

Assertion:

	<assertstmt> ::= assert <expr> [ <string> ]

	"assert <expr> <string>" is completely equivalent to 
	"if !<expr> then error <string> end"

Output statement:

	<putstmt> ::= put ( <expr> | <string> )

Prints out the indicated value, each time the statement is executed.
This is handed straight to printf, so be careful to include a

		  put "\n"

after each line you want to print.

Generally, this will cause a huge amount of stuff to be printed during
verification (with much duplication).  We have used it for debugging,
and for generating a file of all of the possible values of certain
variables (which is then processed to eliminate duplicates).

Function return:

	<returnstmt> ::= return [ <expr> ]

Exit the current procedure, function, rule, or startstate.  If exiting
a function, the <expr> must be provided and must match the return type
of the function; otherwise, there must be no return value.


7. RULES, STARTSTATES, AND INVARIANTS

The syntax for rules, startstates and invariants is as follows:

	<rules> ::= <rule> {; <rule> } [;]
	
	<rule> ::= <simplerule>
	         | <startstate>
		 | <invariant>
		 | <ruleset>
		 | <aliasrule>
	
Simple rule:

	<simplerule> ::= rule [<string>]
			   [ <expr> ==> ]
			   [ { <decl> } begin ]
			   [ stmts ]
			 end

A simple rule determines a transition from one state of the
nondeterministic finite automaton to another.

A simple rule defines a transition between states.  Logically, it
consists of a body, which is a set of statements to be executed, and a
condition, a boolean expression characterizing the states under which
the body may be executed.  If the condition is true in a state, then
the body of the rule may be executed to provide a transition to
another state.

The condition of a rule is optional.  If no condition is specified, then
the rule is assumed to always be enabled.

It is an error to use an expression with side effects in a rule condition.

The rule may declare local variables, constants and types, which are
not part of the state.  If no variables are declared, the begin that
starts the body may be omitted.  Unfortunately, if there is neither a
condition nor local declarations, the parser often misparses the input.
Therefore, rules without conditions should always have the bodies
started with the reserved word begin.

A rule with a condition can be equivalently expressed as a rule
without a condition by the transformation

	rule		   			rule
	  <condition>				  <decls>
	==>					begin
	  <decls>		-->		  if <condition>
	begin					    <body>
	  <body>				  end
	end					end

Although they are functionally redundant, conditions have allowed
speedups in verification by factors of three or four.

It is an error if the program does not have at least one simple rule.

Startstate:

	<startstate> ::= startstate [ <string> ]
		           [ { <decl> } begin ]
			   [ <stmts> ]
			 end

A startstate is a special type of rule.  It is only executed at the
beginning of an execution run.  Another way to phrase this is that
every execution consists of executing one startstate, and then zero or
more simple rules.

A startstate must assign a value to every global variable, or it is
a run-time error which will be caught by the verifier.

It is an error if the program does not have at least one startstate.

Invariant:

	<invariant> ::= invariant [ <string> ] <expr>

The form

    invariant "foo"
      <expr>

is syntactic sugar for

   rule
     !<expr>
   ==>
     Error "Invariant violated: foo"
   end

Many programmers find it more natural to use an embedded specification
style with assert and error statements than to use invariants for some
conditions.  However, for properties that are conveniently expressed
as invariants, it is generally more efficient to express them as
invariants, because the compiler can then take advantage of the
restricted properties of that invariant.

It is an error to use an expression with side effects in an invariant.

Ruleset:

	<ruleset> ::= ruleset <quantifier>
		      {; <quantifier> } do [<rules>] end

A ruleset can be thought of as syntactic sugar for creating a copy
of its component rules for every value of its quantifier.

rule:

	<aliasrule> ::= alias <alias> {; <alias> } do [<rules>] end

An aliased rule creates aliases (see above under the alias
statement) which can be used in all the component rules.


8.  REDUCTION TECHNIQUES

Murphi has two techniques to reduce the memory requirements during
verification: symmetry and multiset reduction, and hash compaction.

8.1 Symmetry and Multiset Reduction

The basic idea of symmetry reduction is that for many protocol one 
can use a reduced state graph for verification instead of the full 
one. Consider, for example, a protocol that has two processors that 
form a list. The state where processor A is the head of the list and B 
is the tail is - for verification purposes - equivalent to the state 
where B is the head and A is the tail. 

Symmetry and multiset reduction are described in more detail in ap-
pendix A and B, respectively. You might also want to look at the
papers ID93.ps and ID93A.ps for more details on symmetry reduction.

8.2 Hash Compaction

When using hash compaction, compressed values are stored in the state 
table instead of full state descriptors. The resulting memory savings
come at the price of a certain probability that some states of the
protocol will be omitted during verification. However, by choosing the
number of bits for the compressed values, the user can control this
probability and make it very small. Furthermore, if one re-runs the
Murphi verifier, the omission probabilities from both runs can be
multiplied, since Murphi picks independent compression functions for 
each run.

There are two different ways how one can use the hash compaction scheme:
- If one wants to have a small bound (typically 0.1%) on the probability 
 of even one omission, typically 40 bits should be used for the com-
 pressed values.
- However, if one is only concerned about the probability of "false 
 positives", i.e. the verifier claiming an error-free protocol even
 though it actually has errors, using only 20 bits is typically suf-
 ficient. 
The verifier reports the actual omission probabilities at the end of 
the verification run. However, the probability of false positives (or 
"even one undetected error") can only be reported when breadth-first 
search is used. Increasing the number of bits by one roughly halves
the reported probabilities.

When using hash compaction together with breadth-first search the infor-
mation needed to generate the error traces can be stored in a temporary 
file ("protocol-name.trace"). The user has to specify the directory for 
this file with the verifier option "-d dir" - otherwise the file will 
not be created and no trace can be printed in the case of a protocol error. 
The memory requirements for each state in this file are the compressed 
value (rounded up to full bytes) plus another 4 bytes.

Remember that you have to compile your protocol with "mu -c" to use
hash compaction. The papers SD95A.ps and SD96A.ps contain more info
on hash compaction. 


A.  SYMMETRY REDUCTION

		   Overview of Symmetry Extension
		
		           C. Norris Ip
 	                    March 1994

Content:

	1) Introduction
	2) Specification of symmetry in Murphi 2.x
		a) new datatype: scalarset
		b) new datatype: scalarsetunion
		c) extended datatypes: undefined value
		d) new operation: undefine
		e) new predicate: isundefine(...)
		f) new predicate: ismember(...)
	3) Verification using symmetry reduction
	4) Underlying mechanism
	5) Things to be aware of for maximium performance
	6) Converting from Murphi 1.x with symmetry
		a) Declaration
		b) Clearing a scalarset/scalarsetunion
		c) ismember(...) and isundefined(...)
	7) Other Files and Directories


1) Introduction:

Symmetry can be used to reduce the amount of time and memory used
in verification.  This document describes how you may take advantage
of symmetry in a system to make verification more efficient.

This document assumes the basic knowledge about Murphi 2.x


2) Specification of symmetry in Murphi 2.x:

a) new datatype: Scalarset

The syntax is as follows:

	typeExpr	: typeid 	/* An already defined type. */
			| enumtype
			| subrangetype
			| recordtype
			| arraytype
	                | scalarsettype	/* scalarset */
			...
			;
		
	scalarsettype   : SCALARSET "(" expr ")" 

You can replace any symmetrical subrange by a scalarset by specifying
its size.  A subrange is symmetrical if all the operations
involving this subrange do not depend on the ordering of the subrange
elements.  For example,

	i) the values are not used in any comparison operation
	   except equality testing, 
	ii) the values are not used in any arithmetic operation, 
	iii) the result from the for loop with the subrange as index
	     does not depend on the order of the iteration.

The compiler will flag an error if you have operations involving a
scalarset that break symmetry.  (Note that in the current
implmentation, the for loop is not checked.)

An example would be the processor id in a multiprocessor system.

	Type
		Proc: Scalarset(NumProc);
	Var
		Processor: Array [Proc] of processor_state;

You cannot use any literal constant to refer to any particular
value in the scalarset.  You can assign value to a scalarset 
variable through the following means:

	i) Forall n : Proc Do ... Endforall
	ii) Exists n : Proc Do ... Endexists
	iii) For n : Proc Do ... Endfor
	iv) Ruleset n : Proc Do ... Endruleset
	v) assignment from another scalarset variables

Note that the "for" construct is a restricted version of the "for"
construct for subrange.  The set of variables written in an iteration
should be disjoint to the set of variables referenced in another
iteration.  The net effect on the variables are therefore independent
to the ordering of the execution of the iterations. There should be no
return statement. 

*** In the current implementation, the user is required ***
*** to check this condition manually.                   ***

b) new datatype: Union

The syntax is as follows:

	typeExpr	: typeid 	/* An already defined type. */
			| enumtype
			| subrangetype
			| recordtype
			| arraytype
	                | scalarsettype	/* scalarset */
	                | uniontype	/* scalarset */
			...
			;
		
	uniontype
        	        : UNION "{" list "}"  
	                ;

	list            : list "," listelt
	                | listelt "," listelt /* at least two elements */ 
	                ; 

	scalarsetlistelt 
	                : ID  		/* scalarset/enum that has 
					already been declared */
			| enumtype

This uniontype provides a short hand if we want to refer
to a few scalarsets at the same time.  For example, in a multiprocessor
system, we will have a set of Memory module and a set of processor.
Then we may want to have channels between every two of them:

	Type
		Mem: Scalarset(NumMem);
		Proc: Scalarset(NumProc);
		Node: Union {Mem, Proc};
	Var
		Channel: Array [Node] of incoming_message;

If we have only 1 Mem, we can use the following:

	Type
		Proc: Scalarset(NumProc);
		Node: Union { enum {Mem} , Proc};
	Var
		Channel: Array [Node] of incoming_message;

c) extended datatypes: undefined value

All base datatype (enumtype, subrangetype, scalarsettype and
uniontype) have been extended to have a undefined value.

This is necessary for scalarsettype and uniontype, because
we have to set the value to a undefined value if they are not used.
(otherwise, the value will be considered in the symmetry consideration
and generates states that are redundant.)

This is also a good extension for other datatypes, because the verifier
can now check that an intentionally undefined value is not used in 
any calculation. (For more detailed explaination, take a look 
at section 5.

d) new operation: undefine

The syntax is as follows:

	undefinestmt	: UNDEFINE designator;

You can set any variable to its respective undefined value using 
"undefine".  If the variable is an aggregate datatype, all 
elements will be set to the undefined value.

e) new predicate: isundefined(...)

The syntax is as follows:

	expr	: ... 
		| ISUNDEFINED '(' designator ')';

You can check whether a variable is undefined using this predicate.
"designator" must be a simple type (enum, subrange, scalarset or
scalarsetunino).

f) new predicate: ismember(...)

The syntax is as follows:

	expr 	: ...
                | ISMEMBER '(' designator ',' typeExpr ')' ;

You can check whether the value of a scalarsetunion variable belongs
to a particular member of the union.  For example you may have:

	Alias n: Message.from Do
		Rule
			Ismember(n,Proc)
			==>
			handle_message_from_processor()
		Endrule;
		Rule
			Ismember(n,Home)
			==> handle_message_from_memory()
		Endrule;
	Endalias;


3) verification using symmetry reduction:

Symmetry reduction is now automatically invoked if appropriate.
You can suppress symmetry reduction by the online flag "-nosym".
You can also change the symmetry reduction algorithm by the
online flag "-sym<n>"
where <n> is the algorithm number for the reduction algorithm.

There are three algorithms provided:

	i) Fast normalization (algorithm 1)
	This algorithm handles the complexity of symmetry reduction
	by an approximation.  Therefore, the time used to canonicalize
	a state is much shorter, while maximium saving is not guaranteed.

	ii) Simple straight-forward canonicalization (algorithm 2)
	This algorithm is used in the papers memtioned at the
	end of this document.  Most of the time it is slower than
	the other algorithms.
	
	iii) Fast canonicalization (algorithm 3)
	This algorithm considers the interrelation between scalarset
	variables in the states and canonicalizes the state much faster
	then algorithm 1,2)

In summary, algorithm 1 is the default.  If it is taking too
long and memory is not a concern, you should try algorithm 3.
If algorithm 1 and 3 give funny error, you have probably discovered
a bug in the new algorithm and you should use algorithm 2.


4) Underlying Mechanism:

The underlying mechanism for symmetry reduction is very simple.

Whenever the standard search algorithm puts a state into the hash
table, we convert it to the unique representative (or, in the case of
normalization, a member in a subset) of the set of symmetry
equivalent states.  Therefore, whenever we check whether 
we have seen a state before, we are checking whether we have
seen an equivalent state before.  If so, we don't do the redundant 
work.

For details, please take a look at "CHDL93.ps" and "ICCD93.ps".


5) Things to be aware of for maximium performance:

You should set variables to their undefined values, if their values
do not affect the functionality of the protocol.

This is always a good practise. Even if we don't have symmetry,
we should set the irrelevent variable to the same value, otherwise
we will have two different states which differ only in this irrelevent
value.  By setting them to the same value, we have a state graph
of a smaller size.

Because we don't have access to a particular value in scalarset, we
have to set it to a value outside the scalarset: the undefined value.

On the other hand, the use of the undefined values
actually caught some of the errors in the examples, which
uses a field in a network message that has not been set by the
sender!
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.