{-

Open Source Fixedpoint Model-Checker version 2009c

(C) Copyright IBM Corp. 2009

All Rights Reserved.

-}

module AnBmain(newanbmain) 
where
import AnBParser
import Ast
import Msg
import Lexer
import System
import Translator
import FPTranslator
import AnBOnP

mkIF :: Protocol -> AnBOptsAndPars -> String
mkIF (protocol@(_,typdec,knowledge,_,_,_)) args = 
            ((if (outt args)==IF 
	      then (\ x -> x++endstr) . ruleList
	      else if ((outt args)==FP) || ((outt args)==FPI) || ((outt args)==Isa)
	      then ruleListFP [] True
	      else error ("Unknown output format: "++(show (outt args))))  . 
	     addInit .
	     addGoals . 
	     rulesAddSteps . 
	     createRules ) (mkPTS protocol args)

newanbmain inputstr otp = 
  (mkIF (anbparser (alexScanTokens inputstr)) otp)

