NuSMV Developers Manual: NuSMV/code/nusmv/shell/bmc/sbmc/sbmcCmd.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``bmc.sbmc'' package of NuSMV version 2.
00005   Copyright (C) 2004 Timo Latvala <timo.latvala@tkk.fi>
00006   Copyright (C) 2006 Tommi Junttila
00007 
00008   NuSMV version 2 is free software; you can redistribute it and/or
00009   modify it under the terms of the GNU Lesser General Public
00010   License as published by the Free Software Foundation; either
00011   version 2 of the License, or (at your option) any later version.
00012 
00013   NuSMV version 2 is distributed in the hope that it will be useful,
00014   but WITHOUT ANY WARRANTY; without even the implied warranty of
00015   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00016   Lesser General Public License for more details.
00017 
00018   You should have received a copy of the GNU Lesser General Public
00019   License along with this library; if not, write to the Free Software
00020   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00021 
00022   For more information of NuSMV see <http://nusmv.fbk.eu>
00023   or email to <nusmv-users@fbk.eu>.
00024   Please report bugs to <nusmv-users@fbk.eu>.
00025 
00026   To contact the NuSMV development board, email to <nusmv@fbk.eu>. 
00027 
00028 -----------------------------------------------------------------------------*/
00029 
00040 #ifndef __NUSMV_SHELL_BMC_SBMC_SBMC_CMD_H__
00041 #define __NUSMV_SHELL_BMC_SBMC_SBMC_CMD_H__
00042 
00043 #if HAVE_CONFIG_H
00044 # include "nusmv-config.h"
00045 #endif
00046 
00047 #include "nusmv/core/utils/utils.h"
00048 #include "nusmv/core/prop/Prop.h"
00049 
00052 /*---------------------------------------------------------------------------*/
00053 /* Function prototypes                                                       */
00054 /*---------------------------------------------------------------------------*/
00055 
00063 void SBmc_AddCmd(NuSMVEnv_ptr env);
00064 
00072 void Sbmc_Cmd_quit(NuSMVEnv_ptr env);
00073 
00150 int
00151 Sbmc_CommandCheckLtlSpecSBmc(NuSMVEnv_ptr env, int argc, char** argv);
00152 
00232 int
00233 Sbmc_CommandGenLtlSpecSBmc(NuSMVEnv_ptr env, int argc, char** argv);
00234 
00288 int
00289 Sbmc_CommandLTLCheckZigzagInc(NuSMVEnv_ptr env, int argc, char** argv);
00290 
00293 #endif /* _BMC_CMD_H */