            de.tla2b.exceptions.TLA2BException
            de.prob.Main
            de.prob.scripting.Api
-           de.be4.classicalb.core.parser.node.AImplicationPredicate))
+           (de.be4.classicalb.core.parser.node TIdentifierLiteral AImplicationPredicate)))
+
+(def varname [(TIdentifierLiteral. "_lambda_result_")])
 
 (def instances 2)
 (def prob-timeout 3000)

(defn mk-formula [formalism input]
  (let [cbf (instantiate formalism input)
        pred? (= "#PREDICATE" (.getKind cbf))]
    (if pred? [cbf nil] (let [gs (str (gensym "ProB_Var_"))] [(instantiate formalism (str gs  " = " input)) gs]))))


(defn top-level-implication? [cbf]

            (serve (get-handler)
                   {:port port
                    :init init
                    :open-browser? false
                    :stacktraces? false
                    :auto-reload? false
                    :destroy destroy
                    :join? true}))))

(defn stop-server []
  (.stop @server)
