Skip to content

Commit

Permalink
some cleaning
Browse files Browse the repository at this point in the history
  • Loading branch information
@Martin-Strecker
Martin-Strecker committed Sep 19, 2021
1 parent 028aebc commit 2198726
Show file tree
Hide file tree
Showing 3 changed files with 38 additions and 105 deletions.
43 changes: 24 additions & 19 deletions src/Exec.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module Exec where
import Data.List
import Syntax
import Typing
import SyntaxManipulation (mkFunTp, abstractF, abstractFvd, liftExpr, dropVar)
import SyntaxManipulation (mkFunTp, abstractF, abstractFvd, liftExpr, dropVar, liftType)
import PrintProg (renameAndPrintExpr, printExpr)
import Data.Maybe (fromMaybe)

Expand All @@ -31,8 +31,8 @@ barithFun ba = case ba of
BAadd -> (+)
BAsub -> (-)
BAmul -> (*)
BAdiv -> (div)
BAmod -> (mod)
BAdiv -> div
BAmod -> mod

bcomparFun :: BComparOp -> Val -> Val -> Bool
bcomparFun bc = case bc of
Expand All @@ -49,8 +49,6 @@ bboolFun bb = case bb of
BBor -> (||)
BBand -> (&&)



liftBArithOp :: BArithOp -> Val -> Val -> Val
liftBArithOp ba c1 c2 = case (c1, c2) of
(IntV i1, IntV i2) -> IntV (barithFun ba i1 i2)
Expand All @@ -64,7 +62,6 @@ liftBBoolOp bb c1 c2 = case (c1, c2) of
(BoolV b1, BoolV b2) -> BoolV (bboolFun bb b1 b2)
_ -> ErrV


liftBinopExpr :: Tp() -> BinOp -> EvalResult (Tp()) -> EvalResult (Tp()) -> Expr (Tp())
liftBinopExpr t bop (ExprResult e1) (ExprResult e2) = case (bop, e1, e2) of
(BArith ba, ValE t1 c1, ValE t2 c2) -> ValE t (liftBArithOp ba c1 c2)
Expand All @@ -73,7 +70,6 @@ liftBinopExpr t bop (ExprResult e1) (ExprResult e2) = case (bop, e1, e2) of
_ -> BinOpE t bop e1 e2
liftBinopExpr t bop _ _ = ValE ErrT ErrV


data EvalResult t
= ExprResult (Expr t)
| ClosResult [EvalResult t] (VarDecl t) (Expr t)
Expand Down Expand Up @@ -105,33 +101,25 @@ evalExpr env x = case x of
ClosResult clenv v fbd -> evalExpr (evalExpr env a:clenv) fbd
FunE t v e -> ClosResult env v e
e -> ExprResult (substClos (map reduceEvalResult env) 0 e)
-- error ((show env) ++ "expr: " ++ (printExpr e))
--

reduceEvalResult :: EvalResult (Tp()) -> Expr (Tp())
reduceEvalResult (ExprResult er) = er
reduceEvalResult (ClosResult clenv v er) = substClos (map reduceEvalResult clenv) 0 (abstractFvd [v] er)

reduceExpr :: Expr (Tp()) -> Expr (Tp())
reduceExpr e = reduceEvalResult (evalExpr [] e)
{-
reduceExpr e = case evalExpr [] e of
ExprResult er -> er
ClosResult clenv v er -> error "reduce does not produce expr"
-- substClos clenv 0 (abstractFvd [v] er)
-}

-- TODO: check if the indexing is correct in the variable case
substClos :: [Expr (Tp())] -> Int -> Expr (Tp()) -> Expr (Tp())
substClos [] _ e = e
substClos env d e@ValE{} = e
substClos env d v@(VarE _ GlobalVar {}) = v
substClos env d ve@(VarE t v@(LocalVar _vn i)) =
if i < d
then ve
else fromMaybe (VarE t (dropVar v)) (lookupEnv (i - d) env)
-- Just (ClosResult nenv v ne) -> error "clos in substClos"
-- substClos nenv 0 (abstractFvd [v] ne)
else fromMaybe (VarE t (dropVar (length env) v)) (lookupEnv (i - d) env)
-- Note: The env corresponds to the number of values being substituted in parallel.
-- When substituting in a local variable of an outer scope, its index
-- has to be decremented by the number of intermediate vars that are eliminated.
substClos env d (UnaOpE t uop e) = UnaOpE t uop (substClos env d e)
substClos env d (BinOpE t bop e1 e2) = BinOpE t bop (substClos env d e1) (substClos env d e2)
substClos env d (IfThenElseE t ec e1 e2) = IfThenElseE t (substClos env d ec) (substClos env d e1) (substClos env d e2)
Expand All @@ -143,3 +131,20 @@ substClos env d (TupleE t es) = TupleE t (map (substClos env d) es)
substClos env d (CastE t ct e) = CastE t ct (substClos env d e)
substClos env d (ListE t lop es) = ListE t lop (map (substClos env d) es)


----------------------------------------------------------------------
-- Tests
----------------------------------------------------------------------

{- For testing evaluation / reduction:
for an assert (P e), reduce expression e
testReduction prg =
let a = head (assertionsOfNewProgram prg)
e = argOfExprAppE (exprOfAssertion a)
ev = evalExpr [] e
in case ev of
ExprResult expr -> putStrLn (printExpr expr)
cl -> do
pPrint cl
putStrLn (printExpr (reduceExpr e))
-}
6 changes: 3 additions & 3 deletions src/SyntaxManipulation.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,9 +138,9 @@ fv (TupleE _ es) = Set.unions (map fv es)
fv (CastE _ _ e) = fv e
fv (ListE _ _ es) = Set.unions (map fv es)

dropVar :: Var t -> Var t
dropVar (LocalVar vn i) = LocalVar vn (i - 1)
dropVar v = v
dropVar :: Int -> Var t -> Var t
dropVar n (LocalVar vn i) = LocalVar vn (i - n)
dropVar n v = v

-- Lift variables and expressions:
-- Increase by one all indices of bound variables with index number >= n
Expand Down
94 changes: 11 additions & 83 deletions src/TimedMC.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@ module TimedMC where
import Syntax
import SyntaxManipulation (conjExpr, disjExpr, implExpr, abstractQ, abstractF, liftVarBy, conjsExpr, disjsExpr, applyVars, mkVarE, mkEq, mkFloatConst, mkFunTp, index, indexListFromTo, gteExpr, eqExpr, mkIntConst, liftVar, funArgsToApp, notExpr)

import PrintProg (renameAndPrintExpr, renameExpr, printExpr)
import PrintProg (renameAndPrintExpr, renameExpr)
import Data.List (find)
import Data.Maybe (fromMaybe)
import Text.Pretty.Simple (pPrint)
import Exec (evalExpr, reduceExpr, EvalResult (ExprResult))
import Exec (reduceExpr)
import Smt (proveExpr)
import KeyValueMap
( selectAssocOfMap, selectAssocOfValue, ValueKVM(MapVM) )
Expand Down Expand Up @@ -106,7 +106,6 @@ constrEFStepAbstrOld fnv stv clvs transv =
(conjExpr (applyVars transv (map (liftVarBy 0 n) sclvsi ++ sclvsi))
(applyVars fnv sclvsi))))

-- TODO: error in liftVarBy ???
constrEFStepAbstr :: TA (Tp()) -> Expr (Tp()) -> Expr (Tp())
constrEFStepAbstr ta fnv =
let n = length (clocksOfTA ta) + 1
Expand All @@ -118,11 +117,6 @@ constrEFStepAbstr ta fnv =
(abstractQ Ex sclvs
(conjExpr (reduceExpr (funArgsToApp (constrTransitions ta) (map mkVarE (map (liftVarBy 0 n) sclvs ++ sclvs))))
(reduceExpr (funArgsToApp fnv (map mkVarE sclvs))))))
-- >>> renameAndPrintExpr [] foo
-- "( \\ st: State -> ( \\ cl1: Time -> ( \\ cl0: Time -> ( exists st_0: State. ( exists cl1_0: Time. ( exists cl0_0: Time. ((((((f st_0@2) cl1_0@1) cl0_0@0) st_0@2) cl1_0@1) cl0_0@0)))))))"

foo :: Expr (Tp ())
foo = let sclvs = (locPar 2) : (clockPars 0 1) in abstractF sclvs (abstractQ Ex sclvs (funArgsToApp (VarE (ClassT {annotOfTp = (), classNameOfTp = ClsNm {stringOfClassName = "State"}}) (GlobalVar {nameOfVar = QVarName {annotOfQVarName = ClassT {annotOfTp = (), classNameOfTp = ClsNm {stringOfClassName = "State"}}, nameOfQVarName = "f"}})) (map mkVarE ((sclvs) ++ sclvs))))

-- Relation composition: for sclvs = [s, c1 .. cn], construct
-- \s \c1 .. \cn \s' \c1' .. \cn' -> exists \s'' \c1'' .. \cn''. r1 s c1 .. cn s'' c1'' .. cn'' && r2 s'' c1'' .. cn'' s' c1' .. cn'
Expand Down Expand Up @@ -218,64 +212,10 @@ checkAutomaton k ta e =
in reduceExpr (funArgsToApp expansion (initialLoc : initialCls))



----------------------------------------------------------------------
-- Tests
----------------------------------------------------------------------


-- BEGIN for testing
mystv :: Var (Tp())
mystv = LocalVar (QVarName integerT "st") 0

mystv' :: Var (Tp())
mystv' = LocalVar (QVarName integerT "st'") 0

myclvs :: [Var (Tp())]
myclvs = [LocalVar (QVarName (ClassT () (ClsNm "Time")) "c1") 0, LocalVar (QVarName (ClassT () (ClsNm "Time")) "c2") 0]

myfnv :: String -> Var (Tp())
myfnv f =
let i = integerT
t = ClassT () (ClsNm "Time")
b = booleanT
in GlobalVar (QVarName (mkFunTp [i, t, t, i, t, t] b) f)

--constrEFStepAbstrTest :: String
--constrEFStepAbstrTest = renameAndPrintExpr [] (constrEFStepAbstr (myfnv "fn") mystv myclvs (myfnv "trans"))

--constrComposTest :: String
--constrComposTest = renameAndPrintExpr [] (constrCompos (mystv : myclvs) (myfnv "r1") (myfnv "r2"))

-- constrDelayTransitionTest :: String
-- constrDelayTransitionTest = renameAndPrintExpr [] (constrDelayTransition myTA mystv myclvs)

myTrans :: Transition (Tp ())
myTrans = Transition (Loc "loc0")
(TransitionGuard [ClConstr (Clock "c1") BCgte 3] trueV)
(TransitionAction Internal [Clock "c2"] (Skip OkT))
(Loc "loc1")

myTA :: TA (Tp ())
myTA = TA OkT "myTA" [Loc "loc0", Loc "loc1"] [] [Clock "c1", Clock "c2"] [myTrans] (Loc "loc0") [(Loc "loc0", [ClConstr (Clock "c1") BClt 3]), (Loc "loc1", [ClConstr (Clock "c2") BClt 2])] []

-- constrActionTransitionTest :: String
-- constrActionTransitionTest = renameAndPrintExpr [] (constrActionTransitions myTA mystv myclvs)

----------------------------------------------------------------------
-- Wiring with rest
----------------------------------------------------------------------

constrAutTransitionTest :: TA (Tp ()) -> String
constrAutTransitionTest ta = renameAndPrintExpr [] (constrTransitions ta)

constrAutGoalTest :: TA (Tp ()) -> Expr (Tp ()) -> String
constrAutGoalTest ta e = renameAndPrintExpr [] (goalFun ta e)

constrAutExpTest :: Int -> TA (Tp ()) -> Expr (Tp ()) -> String
constrAutExpTest k ta e = renameAndPrintExpr [] (checkAutomaton k ta e)

{- For testing formula generation for an automaton -}
runAut :: NewProgram (Tp ()) -> IO ()
{--}
runAut prg =
Expand All @@ -299,27 +239,15 @@ runAut prg =
--runAut prg = putStrLn $ unlines (map constrAutTransitionTest (automataOfNewProgram prg))
-}

{- For testing evaluation / reduction
runAut prg =
let a = head (assertionsOfNewProgram prg)
e = argOfExprAppE (exprOfAssertion a)
ev = evalExpr [] e
in case ev of
ExprResult expr -> putStrLn (printExpr expr)
cl -> do
pPrint cl
putStrLn (printExpr (reduceExpr e))
-}

-- >>> constrActionTransitionTest
-- "( \\ st: Integer -> ( \\ c1: Time -> ( \\ c2: Time -> ( \\ st_0: Integer -> ( \\ c1_0: Time -> ( \\ c2_0: Time -> ((st@5==loc0)&&((st_0@2==loc1)&&(((c1@4>=3)&&True)&&(((c1_0@1==c1@4)&&(c2_0@0==0.0))&&(c2_0@0<2)))))))))))"

{-
( \\ st: Integer -> ( \\ c1: Time -> ( \\ c2: Time -> ( \\ st_0: Integer -> ( \\ c1_0: Time -> ( \\ c2_0: Time ->
((st@5==loc0)&&((st_0@2==loc1)&&(((c1@4>=3)&&True)&&(((c1_0@1==c1@4)&&(c2_0@0==0.0))&&(c2_0@0<2)))))))))))
----------------------------------------------------------------------
-- Tests
----------------------------------------------------------------------

-}
constrAutTransitionTest :: TA (Tp ()) -> String
constrAutTransitionTest ta = renameAndPrintExpr [] (constrTransitions ta)

constrAutGoalTest :: TA (Tp ()) -> Expr (Tp ()) -> String
constrAutGoalTest ta e = renameAndPrintExpr [] (goalFun ta e)

-- END for testing
constrAutExpTest :: Int -> TA (Tp ()) -> Expr (Tp ()) -> String
constrAutExpTest k ta e = renameAndPrintExpr [] (checkAutomaton k ta e)

0 comments on commit 2198726

Please sign in to comment.