verigraph/src/it/polito/verigraph/mcnet/netobjs/PolitoErrFunction.java

   1 /*******************************************************************************
   2  * Copyright (c) 2017 Politecnico di Torino and others.
   3  *
   4  * All rights reserved. This program and the accompanying materials
   5  * are made available under the terms of the Apache License, Version 2.0
   6  * which accompanies this distribution, and is available at
   7  * http://www.apache.org/licenses/LICENSE-2.0
   8  *******************************************************************************/
   9 package it.polito.verigraph.mcnet.netobjs;
  10
  11 import java.util.ArrayList;
  12 import java.util.List;
  13
  14 import com.microsoft.z3.BoolExpr;
  15 import com.microsoft.z3.Context;
  16 import com.microsoft.z3.DatatypeExpr;
  17 import com.microsoft.z3.Expr;
  18 import com.microsoft.z3.FuncDecl;
  19 import com.microsoft.z3.IntExpr;
  20 import com.microsoft.z3.Solver;
  21
  22 import it.polito.verigraph.mcnet.components.NetContext;
  23 import it.polito.verigraph.mcnet.components.Network;
  24 import it.polito.verigraph.mcnet.components.NetworkObject;
  25 /**Error Function objects
  26  *
  27  *
  28  */
  29 public class PolitoErrFunction extends NetworkObject{
  30
  31     List<BoolExpr> constraints;
  32     Context ctx;
  33     DatatypeExpr politoErrFunction;
  34     Network net;
  35     NetContext nctx;
  36     FuncDecl isInBlacklist;
  37
  38     public PolitoErrFunction(Context ctx, Object[]... args) {
  39         super(ctx, args);
  40     }
  41
  42     @Override
  43     protected void init(Context ctx, Object[]... args) {
  44         this.ctx = ctx;
  45         isEndHost=true;
  46         constraints = new ArrayList<BoolExpr>();
  47         z3Node = ((NetworkObject)args[0][0]).getZ3Node();
  48         politoErrFunction = z3Node;
  49         net = (Network)args[0][1];
  50         nctx = (NetContext)args[0][2];
  51         errFunctionRules();
  52         //net.saneSend(this);
  53     }
  54
  55     @Override
  56     public DatatypeExpr getZ3Node() {
  57         return politoErrFunction;
  58     }
  59
  60     @Override
  61     protected void addConstraints(Solver solver) {
  62         //System.out.println("[ERR FUNC] Installing rules.");
  63         BoolExpr[] constr = new BoolExpr[constraints.size()];
  64         solver.add(constraints.toArray(constr));
  65     }
  66
  67     private void errFunctionRules (){
  68         Expr n_0 = ctx.mkConst("PolitoErrFunction_"+politoErrFunction+"_n_0", nctx.node);
  69         Expr p_0 = ctx.mkConst("PolitoErrFunction_"+politoErrFunction+"_p_0", nctx.packet);
  70         IntExpr t_0 = ctx.mkIntConst("PolitoErrFunction_"+politoErrFunction+"_t_0");
  71
  72         //     constraints.add( ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  73         //     ctx.mkImplies((BoolExpr)nctx.send.apply(politoErrFunction, n_0, p_0, t_0),
  74         //                 (BoolExpr)nctx.nodeHasAddr.apply(politoErrFunction, nctx.pf.get("src").apply(p_0))),1,null,null,null,null));
  75         //     constraints.add( ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  76         //     ctx.mkImplies((BoolExpr)nctx.send.apply(politoErrFunction, n_0, p_0, t_0),
  77         //                 ctx.mkEq(nctx.pf.get("origin").apply(p_0), politoErrFunction)),1,null,null,null,null));
  78         //
  79         //     constraints.add( ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  80         //     ctx.mkImplies((BoolExpr)nctx.send.apply(politoErrFunction, n_0, p_0, t_0),
  81         //                    ctx.mkEq(nctx.pf.get("orig_body").apply(p_0),nctx.pf.get("body").apply(p_0))),1,null,null,null,null));
  82
  83
  84         //            Constraint1 We want the ErrFunction not to send out any packet
  85         //    send(politoErrFunction, n_0, p, t_0) -> 1 == 2
  86         constraints.add( ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  87                 ctx.mkImplies((BoolExpr)nctx.send.apply(politoErrFunction, n_0, p_0, t_0),
  88                         ctx.mkEq(ctx.mkInt(1),ctx.mkInt(2))),1,null,null,null,null));
  89
  90         //            constraints.add( ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  91         //            ctx.mkImplies((BoolExpr)nctx.send.apply(n_0, politoErrFunction, p_0, t_0),
  92         //                            (BoolExpr)nctx.nodeHasAddr.apply(politoErrFunction, nctx.pf.get("dest").apply(p_0))),1,null,null,null,null));
  93
  94     }
  95 }
  96