Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
MURPHI2C(1)		    General Commands Manual		   MURPHI2C(1)

NAME
       murphi2c	- translate a Murphi model to C	for simulation

SYNOPSIS
       murphi2c	options	[--output FILE]	[FILE]

DESCRIPTION
       Murphi2C	 is  a utility bundled with the	Rumur model checker. It	can be
       used to translate a Murphi model	into C	source	code  for  integration
       into  a simulator.  The translation is intended to match	the user's in-
       tuition of the C	equivalent of their Murphi model. That	is,  the  pro-
       duced  code  is	more  readable and less	micro-optimised	than the model
       checking	code produced by Rumur itself.

       The C translation produced by Murphi2C is only an approximation of  the
       original	 Murphi	model. For example, there is no	equivalent of the "un-
       defined"	value in C.  If	the input model	relies on  such	 details,  the
       translation will	not precisely match the	model. Similarly the type com-
       patibility rules	for Murphi and C differ, so models that	use aliases or
       rely on type equivalence	may cause Murphi2C to produce C	code that does
       not compile. For	such models, Murphi2C is only intended to generate  an
       initial	skeleton  for  a  C translation. You should always inspect the
       output C	code to	confirm	it matches your	expectations.

       See rumur(1) for	more information about Rumur or	Murphi.

OPTIONS
       --header
	      Generate a C header, as opposed to a source file.

       --output	FILE or	-o FILE
	      Set path to write	the generated C	code to. Without this  option,
	      code is written to stdout.

       --source
	      Generate	a  C  source file, as opposed to a header. This	is the
	      default.

       --value-type TYPE
	      Change the C type	used to	represent scalar values	in the emitted
	      code.  By	 default, int is used. Murphi2C	does not validate that
	      the type you specify is a	valid C	type, but simply  trusts  that
	      you have given something that will be available when you compile
	      the generated code.

       --version
	      Display version information and exit.

NOTES
       The generated C code exposes a set of function  pointers	 that  can  be
       overwritten by other code to control the	behaviour of certain events:

	      // Called	when a model assertion is violated. The	default	imple-
	      mentation	prints
	      // the message and then calls exit().
	      void (*failed_assertion)(const char *message);

	      // Called	when a model assumption	is violated. The  default  im-
	      plementation prints
	      // the message and then calls exit().
	      void (*failed_assumption)(const char *message);

	      // Called	when an	error statement	is reached. The	default	imple-
	      mentation	prints
	      // the message and then calls exit().
	      void (*error)(const char *message);

	      // Called	when a cover condition is hit. The default implementa-
	      tion does
	      // nothing.  void	(*cover)(const char *message);

	      //  Called  when a liveness condition is hit. The	default	imple-
	      mentation	does
	      // nothing.
	      void (*liveness)(const char *message);

       Murphi records are translated into C structs that use native, platform-
       dependent  member  layout.  An  exception to this is if the input model
       performs	aggregate comparisons of record	or array expressions (using ==
       or !=). If this is the case, the	produced structs will be packed	(using
       __attribute__((packed)))	to ensure they can be compared with memcmp.

SEE ALSO
       rumur(1)

AUTHOR
       All comments, questions and complaints should be	 directed  to  Matthew
       Fernandez <matthew.fernandez@gmail.com>.

LICENSE
       This is free and	unencumbered software released into the	public domain.

       Anyone  is  free	 to copy, modify, publish, use,	compile, sell, or dis-
       tribute this software, either in	source code form or as a compiled  bi-
       nary, for any purpose, commercial or non-commercial, and	by any means.

       In  jurisdictions  that recognize copyright laws, the author or authors
       of this software	dedicate any and all copyright interest	in  the	 soft-
       ware  to	 the public domain. We make this dedication for	the benefit of
       the public at large and to the detriment	of our heirs  and  successors.
       We  intend this dedication to be	an overt act of	relinquishment in per-
       petuity of all present and future rights	to this	software  under	 copy-
       right law.

       THE SOFTWARE IS PROVIDED	"AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
       OR IMPLIED, INCLUDING  BUT  NOT	LIMITED	 TO  THE  WARRANTIES  OF  MER-
       CHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN
       NO EVENT	SHALL THE AUTHORS BE LIABLE FOR	ANY CLAIM,  DAMAGES  OR	 OTHER
       LIABILITY, WHETHER IN AN	ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
       FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR  THE	USE  OR	 OTHER
       DEALINGS	IN THE SOFTWARE.

       For more	information, please refer to <http://unlicense.org>

								   MURPHI2C(1)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | NOTES | SEE ALSO | AUTHOR | LICENSE

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=murphi2c&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help