Verif_reverseLinked lists in Verifiable C
Here is a little C program, reverse.c
#include <stddef.h> struct list {unsigned head; struct list *tail;}; struct list *reverse (struct list *p) { struct list *w, *t, *v; w = NULL; v = p; while (v) { t = v->tail; v->tail = w; w = v; v = t; } return w; }
Require Import VST.floyd.proofauto.
Require Import VC.reverse.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Require Import VC.reverse.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Inductive definition of linked lists
Definition t_list := Tstruct _list noattr.
We will define a separation-logic predicate, listrep sigma p,
to describe the concept that the address p in memory is a linked
list that represents the mathematical sequence sigma.
Here, sigma is a list of val, which is C's "value" type:
integers, pointers, floats, etc.
Fixpoint listrep (sigma: list val) (p: val) : mpred :=
match sigma with
| h::hs ⇒
EX y:val, data_at Tsh t_list (h,y) p * listrep hs y
| nil ⇒
!! (p = nullval) && emp
end.
match sigma with
| h::hs ⇒
EX y:val, data_at Tsh t_list (h,y) p * listrep hs y
| nil ⇒
!! (p = nullval) && emp
end.
This says, if sigma has head h and tail hs, then
there is a cons cell at address p with components (h,y).
This cons cell is described by data_at Tsh t_list (h,y) p.
Separate from that, at address y, there is the representation
of the rest of the list, listrep hs y. The memory footprint
for listrep (h::hs) p contains the first cons cell at address p,
and the rest of the cons cells in the list starting at address y.
But if sigma is nil, then p is the null pointer, and the
memory footprint is empty (emp). The fact p=nullval is a pure
proposition (Coq Prop); we inject this into the assertion language
(Coq mpred) using the !! operator.
Because !!P (for a proposition P) does not specify any footprint
(whether empty or otherwise), we do not use the separating conjunction
* to combine it with emp; !!P has no spatial specification
to separate from. Instead, we use the ordinary conjunction &&.
Now, we want to prevent the simpl tactic from automatically
unfolding listrep. This is a design choice that you might make
differently, in which case, leave out the Arguments command.
Arguments listrep sigma p : simpl never.
Hint databases for spatial operators
- The saturate_local hint is a lemma that extracts pure propositional facts from a spatial fact.
- The valid_pointer hint is a lemma that extracts a valid-pointer fact from a spatial lemma.
Lemma data_at_isptr_example1:
∀(h y p : val) ,
data_at Tsh t_list (h,y) p ⊢- !! isptr p.
Proof.
intros.
∀(h y p : val) ,
data_at Tsh t_list (h,y) p ⊢- !! isptr p.

Qed.
Lemma data_at_isptr_example2:
∀(h y p : val) ,
data_at Tsh t_list (h,y) p ⊢- !! isptr p.
Proof.
intros.
Qed.
Lemma data_at_isptr_example2:
∀(h y p : val) ,
data_at Tsh t_list (h,y) p ⊢- !! isptr p.
Proof.
intros.
Let's look more closely at how entailer! solves this goal.
First, it finds all the pure propositions Prop that it can deduce from the
mpred conjuncts on the left-hand side, and puts them above the line.
saturate_local.
The saturate_local tactic uses a Hint database (also called saturate_local)
to look up the individual conjuncts on the left-hand side (this particular entailment
has just one conjunct).
Print HintDb saturate_local.
In this case, the new propositions above the line are labeled H and H0. Next, if the proof goal has just a proposition !!P on the right,
entailer! throws away the left-hand-side and tries to prove P.
(This is rather aggressive, and can sometimes lose information, that is,
sometimes entailer! will turn a provable goal into an unprovable goal.)
apply prop_right.
It happens that field_compatible _ _ p implies isptr p,
Check field_compatible_isptr.
(* : forall (t : type) (path : list gfield) (p : val),
field_compatible t path p -> isptr p *)
(* : forall (t : type) (path : list gfield) (p : val),
field_compatible t path p -> isptr p *)
So therefore, field_compatible_isptr solves the goal.
eapply field_compatible_isptr; eauto.
(* Now you have some insight into how entailer! works. *)
Qed.
(* Now you have some insight into how entailer! works. *)
Qed.
But when you define a new spatial predicate mpred such as listrep,
the saturate_local tactic does not know how to deduce Prop facts
from the listrep conjunct:
Lemma listrep_facts_example:
∀sigma p,
listrep sigma p ⊢- !! (isptr p ∨ p=nullval).
Proof.
intros.
entailer!.
∀sigma p,
listrep sigma p ⊢- !! (isptr p ∨ p=nullval).
Proof.
intros.
entailer!.
Here, entailer! threw away the left-hand-side and left an unprovable goal.
Let's see why.
Abort.
Lemma listrep_facts_example:
∀sigma p,
listrep sigma p ⊢- !! (isptr p ∨ p=nullval).
Proof.
intros.
Lemma listrep_facts_example:
∀sigma p,
listrep sigma p ⊢- !! (isptr p ∨ p=nullval).
Proof.
intros.
First entailer! would use saturate_local to see (from the Hint database)
what can be deduced from listrep sigma p.
saturate_local.
But saturate_local did not add anything above the line. That's because
there's no Hint in the Hint database for listrep.
Therefore we must add one. The conventional name for such a lemma
is f_local_facts, if your new predicate is named f.
Abort.

For each spatial predicate Definition f(_): mpred,
there should be one "local fact", a lemma of the form
f(_) ⊢- !! _. On the right hand side, put all the propositions
you can derive from f(_). In this case, we know:
- p is either a pointer or null (it's never Vundef, or Vfloat, or a nonzero Vint).
- p is null, if and only if sigma is nil.
Proof.
intros.
intros.
We will prove this entailment by induction on sigma
revert p; induction sigma; intros p.
- (** In the base case, sigma is nil. We can unfold the definition
of listrep to see what that means. *)
unfold listrep.
- (** In the base case, sigma is nil. We can unfold the definition
of listrep to see what that means. *)
unfold listrep.
Now we have an entailment with a proposition p=nullval on the left.
To move that proposition above the line, we could do Intros, but
it's easier just to call on entailer! to see how it can simplify (and perhaps
partially solve) this entailment goal:
entailer!.
(* The entailer! has left an ordinary proposition, which is easy to solve. *)
split; auto.
- (** In the inductive case, we can again unfold the definition
of listrep (a::sigma); but then it's good to fold listrep sigma.
Replace the semicolon ; with a period in the next line, to see why. *)
unfold listrep; fold listrep.
(* The entailer! has left an ordinary proposition, which is easy to solve. *)
split; auto.
- (** In the inductive case, we can again unfold the definition
of listrep (a::sigma); but then it's good to fold listrep sigma.
Replace the semicolon ; with a period in the next line, to see why. *)
unfold listrep; fold listrep.
Warning! Sometimes entailer! is too aggressive. If we use it
here, it will throw away the left-hand side because it doesn't
understand how to look inside an EXistential quantitier. The
exclamation point ! is a warning that entailer! can turn a
provable goal into an unprovable goal. Uncomment the next line
and see what happens. Then put the comment marks back.
(* entailer!. *)
The preferred way to handle EX y:t on the left-hand-side of an
entailment is to use Intros y.
(* Intros y. *)
A less agressive entailment-reducer is entailer without the
exclamation point. This one never turns a provable goal into an
unprovable goal. Here it will Intro the EX-bound variable y.
entailer.
Should you use entailer! or entailer in ordinary proofs?
Usually entailer! is best: it's faster, and it does more work for you.
Only if you find that entailer! has gone into a dead end, should
you use entailer instead.
Here it is safe to use entailer!
entailer!.
Notice that entailer! has put several facts above the line:
field_compatible t_list [] p and value_fits t_list (a,y) come from the
saturate_local hint database, from the data_at conjunct; and
is_pointer_or_null y and y=nullval ↔ sigma=[] come from the
the listrep conjunct, using the induction hypothesis IHsigma.
Now, let's split the goal and take the two cases separately.
split; intro.
*
clear - H H2.
subst p.
*
clear - H H2.
subst p.
It happens that field_compatible _ _ p implies isptr p,
Check field_compatible_isptr.
(* : forall (t : type) (path : list gfield) (p : val),
field_compatible t path p -> isptr p *)
(* : forall (t : type) (path : list gfield) (p : val),
field_compatible t path p -> isptr p *)
The predicate isptr excludes the null pointer,
Print isptr.
(* = fun v : val => match v with Vptr _ _ => True | _ => False end *)
Print nullval.
(* = if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero *)
(* = fun v : val => match v with Vptr _ _ => True | _ => False end *)
Print nullval.
(* = if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero *)
Therefore H is a contradiction. We can proceed with,
Check field_compatible_nullval.
(* = forall (CS : compspecs) (t : type) (f : list gfield) (P : Type),
field_compatible t f nullval -> P *)
eapply field_compatible_nullval; eauto.
* (*The case a::sigma=[] → p=nullval is easy, by inversion: *)
inversion H2.
Qed.
(* = forall (CS : compspecs) (t : type) (f : list gfield) (P : Type),
field_compatible t f nullval -> P *)
eapply field_compatible_nullval; eauto.
* (*The case a::sigma=[] → p=nullval is easy, by inversion: *)
inversion H2.
Qed.
Now we add this lemma to the Hint database called saturate_local
Hint Resolve listrep_local_facts : saturate_local.
Valid pointers, and the valid_pointer Hint database
Lemma struct_list_valid_pointer_example:
∀h y p,
data_at Tsh t_list (h,y) p ⊢- valid_pointer p.
Proof.
intros.
auto with valid_pointer.
Qed.
∀h y p,
data_at Tsh t_list (h,y) p ⊢- valid_pointer p.
Proof.
intros.
auto with valid_pointer.
Qed.
However, the hint database does not know about user-defined
separation-logic predicates (mpred) such as listrep; for example:
Lemma listrep_valid_pointer_example:
∀sigma p,
listrep sigma p ⊢- valid_pointer p.
Proof.
intros.
auto with valid_pointer.
∀sigma p,
listrep sigma p ⊢- valid_pointer p.
Proof.
intros.
auto with valid_pointer.
Notice that auto with... did not solve the proof goal
Abort.
Therefore, we should prove the appropriate lemma, and add it to the
Hint database.
Lemma listrep_valid_pointer:
∀sigma p,
listrep sigma p ⊢- valid_pointer p.
Proof.
intros.
∀sigma p,
listrep sigma p ⊢- valid_pointer p.
Proof.
intros.
The main point is to unfold listrep.
unfold listrep.
Now we can prove it by case analysis on sigma; we don't even need
induction.
destruct sigma; simpl.
* (** The nil case is easy: *)
hint.
entailer!.
* (** The cons case *)
Intros y.
* (** The nil case is easy: *)
hint.
entailer!.
* (** The cons case *)
Intros y.
Now this solves using the Hint database valid_pointer, because the
data_at Tsh t_list (v,y) p on the left is enough to prove the goal.
auto with valid_pointer.
Qed.
Qed.
Now we add this lemma to the Hint database
Hint Resolve listrep_valid_pointer : valid_pointer.
Specification of the reverse function.
A funspec characterizes the precondition required for calling the function and the postcondition guaranteed by the function.
Definition reverse_spec : ident * funspec :=
DECLARE _reverse
WITH sigma : list val, p: val
PRE [ _p OF (tptr t_list) ]
PROP ()
LOCAL (temp _p p)
SEP (listrep sigma p)
POST [ (tptr t_list) ]
EX q:val,
PROP () LOCAL (temp ret_temp q)
SEP (listrep(rev sigma) q).
DECLARE _reverse
WITH sigma : list val, p: val
PRE [ _p OF (tptr t_list) ]
PROP ()
LOCAL (temp _p p)
SEP (listrep sigma p)
POST [ (tptr t_list) ]
EX q:val,
PROP () LOCAL (temp ret_temp q)
SEP (listrep(rev sigma) q).
- The WITH clause says, there is a value sigma: list val and a value p: val, visible in both the precondition and the postcondition.
- The PREcondition says,
- There is a single function-parameter named _p, whose C type is "pointer to struct list"
- LOCAL: The C local variable _p contains the Coq value p;
- SEP: in memory at address p there is a linked list representing sigma.
- The POSTcondition says,
- the function returns a value whose C type is "pointer to struct list"; and
- there exists a value q: val, such that
- LOCAL: the "return temporary", a pseudovariable holdingthe function's return value, holds the value q
- SEP: in memory at address q there is a linked list representing rev sigma.
Definition Gprog : funspecs :=
ltac:(with_library prog [ reverse_spec ]).
ltac:(with_library prog [ reverse_spec ]).
Proof of the reverse function
Lemma body_reverse: semax_body Vprog Gprog
f_reverse reverse_spec.
Proof.
f_reverse reverse_spec.
Proof.
The start_function tactic "opens up" a semax_body
proof goal into a Hoare triple.
start_function.
As usual, the current assertion (precondition) is derived
from the PRE clause of the function specification, reverse_spec,
and the current command w=0; ...more... is the function
body of f_reverse.
The first statement (command) in the function-body is the assignment
statement w=NULL;, where NULL is a C #define that exands to
"cast 0 to void-pointer", (void * )0, here ugly-printed as (tptr tvoid)(0).
To apply the separation-logic assignment rule to this command, simply
use the tactic forward :
forward. (* w = NULL; *)
The new semax judgment is for the rest of the function body after
the command w=NULL. The precondition of this semax is actually
the postcondition of the w=NULL statement. It's much like the
precondition of w=NULL, but contains the additional LOCAL fact,
temp _w (Vint (Int.repr 0)), that is, the local variable _w contains nullval.
We can view the Hoare-logic proof of this program as a "symbolic execution",
where the symbolic states are assertions. We can symbolically execute
the next command by saying forward again.
forward. (* v = p; *)
Examine the precondition, and notice that now we have the additional
fact, temp _v p.
We cannot the next step using forward ...
Fail forward.
... because the next command is a while loop.
To prove a while-loop, you must supply a loop invariant,
in this case (EX s1 PROP(...)LOCAL(...)(SEP(...)).
forward_while
(EX s1: list val, EX s2 : list val,
EX w: val, EX v: val,
PROP (sigma = rev s1 ++ s2)
LOCAL (temp _w w; temp _v v)
SEP (listrep s1 w; listrep s2 v)).
(EX s1: list val, EX s2 : list val,
EX w: val, EX v: val,
PROP (sigma = rev s1 ++ s2)
LOCAL (temp _w w; temp _v v)
SEP (listrep s1 w; listrep s2 v)).
The forward_while tactic leaves four subgoals,
which we mark with * (the Coq "bullet")
* (* Prove that (current) precondition implies the loop invariant *)
hint.
hint.
On the left-hand side of this entailment is the precondition
(that we had already established by forward symbolic execution to this
point) for the entire while-loop. On the right-hand side is the loop
invariant, that we just gave to the forward_while tactic. Because
the right_hand side has for existentials, a good proof strategy is to
choose values for them, using the Exists tactic.
Exists (@nil val) sigma nullval p.
Now we have a quantifier-free proof goal; let us see whether entailer!
can solve some parts of it.
entailer!.
Indeed, the entailer! did a fine job. What's left is a property of our
user-defined listrep predicate: emp ⊢- listrep [] nullval.
unfold listrep.
Now that the user-defined predicate is unfolded, entailer! can solve
the residual entailment.
entailer!.
* (* Prove that loop invariant implies typechecking of loop condition *)
hint.
* (* Prove that loop invariant implies typechecking of loop condition *)
hint.
The second subgoal of forward_while is to prove that the loop-test
condition can execute without crashing. Consider, for example,
the C-language while loop, while (a[i]>0) ..., where the value of i
might exceed the bounds of the array. Then this would be a
"buffer overrun", and is "undefined behavior" ("stuck") in the C semantics.
We must prove that, given the current precondition (in this case,
the loop invariant), the loop test is not "undefined behavior."
This proof goal takes the form, current-precondition ⊢- tc_expr Delta e,
where e is the loop-test expression. You can pronounce tc_expr as
"type-check expression", since the Verifiable C type-checker ensures
that such expressions are safe (sometimes with a subgoal for you to prove).
Fortunately, in most cases the entailer! solves tc_expr goals
completely automatically:
entailer!.
* (* Prove that loop body preserves invariant *)
hint.
* (* Prove that loop body preserves invariant *)
hint.
As usual in any Hoare logic (including Separation Logic), we need to prove
that the loop body preserves the loop invariant, more precisely,
The loop invariant was EX s1:_, EX s2:_, EX w:_, EX v:_, ..., and here
all the existentially quantified variables on the left side of the entailment
have been moved above the line: s1, s2: val and w,v: val.
The PROP part of the loop invariant was sigma = rev s1 ++ s2, and
it has also been moved above the line, as hypothesis H.
So now we would like to do forward-symbolic execution through
the four assignment statements in the loop body.
- {Inv /\ Test} body {Inv}
Fail forward.
But we cannot go forward through t=v→tail; because that would
require a SEP conjunct in the precondition of the form
data_at sh t_list (_,_) v, and there is no such conjunct. Actually,
there is such a conjunct, but it is hiding inside listrep s2 v.
That is, there is such a conjunct as long as s2 is not nil.
Let's do case analysis on s2:
destruct s2 as [ | h r].
- (* s2=nil *)
(** Suppose s2=nil. If we unfold listrep . . . *)
unfold listrep at 2.
- (* s2=nil *)
(** Suppose s2=nil. If we unfold listrep . . . *)
unfold listrep at 2.
then we learn that v=nullval. To move this fact (or any proposition)
from the precondition to above-the-line, we use Intros:
Intros.
Now, above the line, we have v=nullval and isptr v; this is a contradiction.
subst. contradiction.
- (* s2=h::r *)
(** Suppose s2=h::r. We can unfold/fold the listrep conjunct for h::r;
if you don't remember why we do unfold/fold, then replace the semicolon
(between the fold and the unfold) with a period and see what happens. *)
unfold listrep at 2; fold listrep.
- (* s2=h::r *)
(** Suppose s2=h::r. We can unfold/fold the listrep conjunct for h::r;
if you don't remember why we do unfold/fold, then replace the semicolon
(between the fold and the unfold) with a period and see what happens. *)
unfold listrep at 2; fold listrep.
By the definition of listrep, at address v there must exist a value y
and a list cell containing (h,y). So let us move y above the line:
Intros y.
Now we have the appropriate SEP conjuncts to be able to go forward
through the loop body
forward. (* t = v->tail *)
forward. (* v->tail = w; *)
forward. (* w = v; *)
forward. (* v = t; *)
forward. (* v->tail = w; *)
forward. (* w = v; *)
forward. (* v = t; *)
At the end of loop body; we must reestablish the loop invariant.
The left-hand-side of this entailment is the current assertion (after
the loop body); the right-hand side is simply our loop invariant.
(Unfortunately, the forward_while tactic has "uncurried" the existentials
into a single EX that binds a 4-tuple.)
Since the proof goal is a complicated-looking entailment, let's see
if entailer! can simplify it a bit:
entailer!.
Now, we can provide new values for s1,s2,w,v to instantiate the
four existentials; these are, respectively, h::s1,r,v,y.
Exists (h::s1,r,v,y).
Again, we have a complicated-looking entailment; we ask entailer!
to reduce it some more.
entailer!.
+ simpl. rewrite app_ass. auto.
+ unfold listrep at 3; fold listrep.
Exists w. entailer!.
* (* after the loop *)
(** As usual in any Hoare logic (including Separation Logic), the postcondition
of a while-loop is {Inv /\ not Test}, where Inv is the loop invariant
and Test is the loop test. Here, all the EXistentials and PROPs of the
loop invariant have been moved above the line as s1,s2,w,v,HRE,H.
We can always go forward through a return statement: *)
forward. (* return w; *)
+ simpl. rewrite app_ass. auto.
+ unfold listrep at 3; fold listrep.
Exists w. entailer!.
* (* after the loop *)
(** As usual in any Hoare logic (including Separation Logic), the postcondition
of a while-loop is {Inv /\ not Test}, where Inv is the loop invariant
and Test is the loop test. Here, all the EXistentials and PROPs of the
loop invariant have been moved above the line as s1,s2,w,v,HRE,H.
We can always go forward through a return statement: *)
forward. (* return w; *)
Now we must prove that the current assertion (after the while-loop)
entails the function postcondition. The left-hand side of this entailment
is what we had just before forward through the return;
the right-hand side is the postcondition of reverse_spec,
after the local variables (etc.) have been simplified away. We must
demonstrate a pointer q (here it's called x) that satisfies the various
conditions. Here it's easy to find x, since it's constrained to be
equal to w:
Exists w; entailer!.
rewrite (proj1 H1) by auto.
unfold listrep at 2; fold listrep.
entailer!.
rewrite <- app_nil_end, rev_involutive.
auto.
Qed.
rewrite (proj1 H1) by auto.
unfold listrep at 2; fold listrep.
entailer!.
rewrite <- app_nil_end, rev_involutive.
auto.
Qed.
Why separation logic?
Fixpoint listrep (sigma: list val) (p: val) : mpred :=
match sigma with
| h::hs ⇒
EX y:val, data_at Tsh t_list (h,y) p * listrep hs y
| nil ⇒
!! (p = nullval) && emp
end.
In the nonempty list case, the head element is described by
match sigma with
| h::hs ⇒
EX y:val, data_at Tsh t_list (h,y) p * listrep hs y
| nil ⇒
!! (p = nullval) && emp
end.
data_at Tsh t_list (h,y) p
which is separated (by the separating conjunction * ) from the rest of the list
listrep hs y.
This separation ensures that no address could be used for more than once in a
linked list. For example, considering a linked list of length at least 2,
listrep (a :: b :: l) x.
We know that there must be two addresses y and z such that
data_at Tsh t_list (a,y) x *
data_at Tsh t_list (b,z) y *
listrep l z.
The "separating conjunction" * tells us that x and y must be different!
Formally, we can prove the following two lemmas:
data_at Tsh t_list (b,z) y *
listrep l z.
Lemma listrep_len_ge2_fact: ∀(a b x: val) (l: list val),
listrep (a :: b :: l) x ⊢-
EX y: val, EX z: val,
data_at Tsh t_list (a,y) x *
data_at Tsh t_list (b,z) y *
listrep l z.
Proof.
intros.
unfold listrep; fold listrep.
Intros y z.
Exists y z.
cancel.
Qed.
Lemma listrep_len_ge2_address_different: ∀(a b x y z: val) (l: list val),
data_at Tsh t_list (a,y) x *
data_at Tsh t_list (b,z) y *
listrep l z ⊢-
!! (x ≠ y).
Proof.
intros.
listrep (a :: b :: l) x ⊢-
EX y: val, EX z: val,
data_at Tsh t_list (a,y) x *
data_at Tsh t_list (b,z) y *
listrep l z.
Proof.
intros.
unfold listrep; fold listrep.
Intros y z.
Exists y z.
cancel.
Qed.
Lemma listrep_len_ge2_address_different: ∀(a b x y z: val) (l: list val),
data_at Tsh t_list (a,y) x *
data_at Tsh t_list (b,z) y *
listrep l z ⊢-
!! (x ≠ y).
Proof.
intros.
To prove that the addresses are different, we do case analysis first.
If x = y, we use the following theorem:
Check data_at_conflict.
(* : forall (sh : Share.t) (t : type) (v v' : reptype t) (p : val),
sepalg.nonidentity sh -> 0 < sizeof t ->
data_at sh t v p * data_at sh t v' p ⊢- FF *)
(* : forall (sh : Share.t) (t : type) (v v' : reptype t) (p : val),
sepalg.nonidentity sh -> 0 < sizeof t ->
data_at sh t v p * data_at sh t v' p ⊢- FF *)
It says that we can derives address anti-aliasing from the "separation"
defined by *. If x ≠ y, the right side is already proved.
destruct (Val.eq x y); [| apply prop_right; auto].
subst x.
sep_apply (data_at_conflict Tsh t_list (a, y)).
+ auto.
+ entailer!.
Qed.
(* Actually, even the property x≠y is not strong enough! We need to
know that x does not overlap with _any field_ of record y,
for example (in C notation) x != &(y→tail) and &(x→tail) != y.
Otherwise, when storing into y→tail, we couldn't know that x→head
is not altered. *)
subst x.
sep_apply (data_at_conflict Tsh t_list (a, y)).
+ auto.
+ entailer!.
Qed.
(* Actually, even the property x≠y is not strong enough! We need to
know that x does not overlap with _any field_ of record y,
for example (in C notation) x != &(y→tail) and &(x→tail) != y.
Otherwise, when storing into y→tail, we couldn't know that x→head
is not altered. *)
Without separation logic, we could still define listrep' using extra
clauses for address anti-aliasing. For example, a length-3 linked list
listrep (a :: b :: c :: nil) x can be: exists y and z, such that (a, y)
is stored at x, (b, z) is stored at y, (c, nullval) is stored at z and
x, y and z are different from each other. In general, that assertion will
be quadratically long (as a function of the length of the linked list).
Then, to make sure x→head is not at the same address as y→tail, we'd need
even more assertions.
In our program correctness proof, we do (implicitly) use the fact that
different SEP clauses describe disjoint heaplets. Here is an
intermediate step in the proof of body_reverse.
(We rarely state intermediate proof goals such as this one.
We do it here to illustrate a point about separating conjunction.
Lemma body_reverse_step: ∀
{Espec : OracleKind}
(sigma : list val)
(s1 : list val)
(h : val)
(r : list val)
(w v : val)
(HRE : isptr v)
(H : sigma = rev s1 ++ h :: r)
(y : val),
semax (func_tycontext f_reverse Vprog Gprog nil)
(PROP ( )
LOCAL (temp _t y; temp _w w; temp _v v)
SEP (listrep s1 w; data_at Tsh t_list (h, y) v; listrep r y))
(Ssequence
(Sassign
(Efield
(Ederef (Etempvar _v (tptr (Tstruct _list noattr))) (Tstruct _list noattr))
_tail (tptr (Tstruct _list noattr)))
(Etempvar _w (tptr (Tstruct _list noattr))))
(Ssequence (Sset _w (Etempvar _v (tptr (Tstruct _list noattr))))
(Sset _v (Etempvar _t (tptr (Tstruct _list noattr))))))
(normal_ret_assert
(PROP ( )
LOCAL (temp _v y; temp _w v; temp _t y)
SEP (listrep s1 w; data_at Tsh t_list (h, w) v; listrep r y))).
Proof.
intros.
abbreviate_semax.
{Espec : OracleKind}
(sigma : list val)
(s1 : list val)
(h : val)
(r : list val)
(w v : val)
(HRE : isptr v)
(H : sigma = rev s1 ++ h :: r)
(y : val),
semax (func_tycontext f_reverse Vprog Gprog nil)
(PROP ( )
LOCAL (temp _t y; temp _w w; temp _v v)
SEP (listrep s1 w; data_at Tsh t_list (h, y) v; listrep r y))
(Ssequence
(Sassign
(Efield
(Ederef (Etempvar _v (tptr (Tstruct _list noattr))) (Tstruct _list noattr))
_tail (tptr (Tstruct _list noattr)))
(Etempvar _w (tptr (Tstruct _list noattr))))
(Ssequence (Sset _w (Etempvar _v (tptr (Tstruct _list noattr))))
(Sset _v (Etempvar _t (tptr (Tstruct _list noattr))))))
(normal_ret_assert
(PROP ( )
LOCAL (temp _v y; temp _w v; temp _t y)
SEP (listrep s1 w; data_at Tsh t_list (h, w) v; listrep r y))).
Proof.
intros.
abbreviate_semax.
Now, our proof goal is:
semax Delta
(PROP ( )
LOCAL (temp _t y; temp _w w; temp _v v)
SEP (listrep s1 w; data_at Tsh t_list (h, y) v; listrep r y))
((_v → _tail) = _w;
MORE_COMMANDS) POSTCONDITION.
The next forward tactic will execute a symbolic execution for v→tail = w.
(PROP ( )
LOCAL (temp _t y; temp _w w; temp _v v)
SEP (listrep s1 w; data_at Tsh t_list (h, y) v; listrep r y))
((_v → _tail) = _w;
MORE_COMMANDS) POSTCONDITION.
forward. (* v->tail = w; *)
It turns the precondition into:
Because they are separated! The separation ensures that address v is not used
in the linked list described by listrep s1 w.
PROP ( )
LOCAL (temp _t y; temp _w w; temp _v v)
SEP (listrep s1 w; data_at Tsh t_list (h, w) v; listrep r y).
It is no problem that the separating conjunct data_at Tsh t_list (h, y) v is
turned into data_at Tsh t_list (h, w) v. But why weren't the other separating
conjuncts like listrep s1 w affected?
LOCAL (temp _t y; temp _w w; temp _v v)
SEP (listrep s1 w; data_at Tsh t_list (h, w) v; listrep r y).
Abort.
When C programs manipulate pointer data structures (or slices of arrays),
address anti-aliasing plays an important role in their correctness proofs.
Separation logic is essential for reasoning about updates to these structures.
Verifiable C's SEP clause ensures separation between all its conjuncts.
(* Wed Apr 24 08:45:36 EDT 2019 *)


account_balance
Core Banking API
menu
Home
Services Available
Technologies used
Home
Services Available
Technologies used
Payments made Easy
Fast.Secure.Reliable
Core Banking API for Fintech Integration
recent_actors
Register here
Click here to register for payment features
remove_circle
Deregister
Click here to stop using services
payment
Payment Authorization
Click here to authorize your payments
backspace
Payment reversal
Click here to reverse your transaction


Annotations
Instead of writing a lot of reflection code you can use annotations to define your original and patch methods in a declarative way. Harmony uses annotations in a hierarchical way on classes and methods in those classes to determine which original methods you want to patch with which patch methods and with which properties like priorities and such.
To simplify things, each original method you want to patch is usually represented by a "patch class", that is, a class that has at least one harmony patch annotation [HarmonyPatch]
.
When you call harmony.PatchAll(), Harmony will search through all classes and methods inside the given assembly looking for specific Harmony annotations, applying all patch classes that it finds.
To selectively apply certain patch classes, harmony.PatchCategory() can be used with [HarmonyPatchCategory]
to mark specific patch classes to apply. Alongside this, harmony.PatchAllUncategorized() can be used to apply patch classes not marked with a specific category. Note that harmony.PatchAll() ignores categories.
A typical patch consists of a class with annotations that looks like this:
using HarmonyLib;
[HarmonyPatch(typeof(SomeTypeHere))]
[HarmonyPatch("SomeMethodName")] // if possible use nameof() here
class MyPatches
{
static void Postfix(/*...*/)
{
//...
}
}
This example annotates the class with enough information to identify the method to patch. Inside that class, you define a combination of Prefix, Postfix, Finalizer or Transpiler methods. Harmony will find them by their name and if you annotate those methods you can even have different names.
Patch classes
Patch classes can be public, private, static or not. Patch methods can be public or private but must be static since the patched original method does not have any reference to an instance of your patch class. If you use the manual way to specify the patch methods, your patch methods can even be DynamicMethod's.
Limitations
The only limitation is that annotations are not ordered (even if they appear so). At runtime, the order of methods or multiple annotations on something is undefined. The consequence of this is that you cannot rely on order when you define multiple annotations that theoretically could overwrite each other like with normal inheritance. This normally isn't a problem unless you annotate multiple Prefix methods in a class and expect the order of the prefixes to be as in the source code (use priority annotations in this case).
Annotation alternatives
To indicate that a class contains patch methods it needs to be annotated with at lease one annotations.
Basic annotations
Basic annotations need to be combined to define all aspects of your original method:
Empty annotation
// The empty annotation marks the class as a patch class. Harmony will consider the class and its methods.
[HarmonyPatch]
Class/Type annotation
// Use the type annotation to define the class/type that contains your original method/property/constructor
[HarmonyPatch(Type declaringType)]
Name annotation
// Use the string annotation to define the name of the method or property
[HarmonyPatch(string methodName)]
// or for methods with overloads add an optional argument type array:
[HarmonyPatch(string methodName, params Type[] argumentTypes)]
Method Type annotation
// Defines the type (Method, Getter, Setter, Constructor) to be patched
[HarmonyPatch(MethodType methodType)]
Arguments annotation
// For overloads this defines the argument types of the method/constructor
[HarmonyPatch(Type[] argumentTypes)]
// Since annotations cannot contain code and you cannot use .MakeByRefType(), the second
// form allows for a ArgumentType array defining the type of each argument type
// Normal, Ref, Out or Pointer. Both arrays need to have the same number of elements:
[HarmonyPatch(Type[] argumentTypes, ArgumentType[] argumentVariations)]
Category annotation
// Use with Harmony.PatchCategory()
[HarmonyPatchCategory(string category)]
Combination annotations
Beside combining the basic annotations you can also pick from the many combination annotations to express things more compact:
[HarmonyPatch(Type, string)]
[HarmonyPatch(Type declaringType, Type[] argumentTypes)]
[HarmonyPatch(Type declaringType, string methodName)]
[HarmonyPatch(Type declaringType, string methodName, params Type[] argumentTypes)]
[HarmonyPatch(Type declaringType, string methodName, Type[] argumentTypes, ArgumentType[] argumentVariations)]
[HarmonyPatch(Type declaringType, MethodType methodType)]
[HarmonyPatch(Type declaringType, MethodType methodType, params Type[] argumentTypes)]
[HarmonyPatch(Type declaringType, MethodType methodType, Type[] argumentTypes, ArgumentType[] argumentVariations)]
[HarmonyPatch(string methodName, Type[] argumentTypes, ArgumentType[] argumentVariations)]
[HarmonyPatch(string methodName, MethodType methodType)]
[HarmonyPatch(MethodType methodType, params Type[] argumentTypes)]
[HarmonyPatch(MethodType methodType, Type[] argumentTypes, ArgumentType[] argumentVariations)]
Examples
To patch method String.ToUpper() :
[HarmonyPatch(typeof(String))]
[HarmonyPatch("ToUpper")]
To patch the setter for a property Account in class MyClass :
[HarmonyPatch(typeof(MyClass))]
[HarmonyPatch("Account", MethodType.Setter)]
To patch method String.IndexOf(char, int) :
[HarmonyPatch(typeof(String))]
[HarmonyPatch("IndexOf")]
[HarmonyPatch(new Type[] { typeof(char), typeof(int) })]
//or
[HarmonyPatch(typeof(String), "IndexOf", new Type[] { typeof(char), typeof(int) })]
Constructors
To patch constructors, you use the annotations that contain a MethodType
argument and set it to MethodType.Constructor
:
// default constructor:
[HarmonyPatch(typeof(TestClass), MethodType.Constructor)]
// or with an overload:
[HarmonyPatch(typeof(TestClass), MethodType.Constructor, new Type[] { typeof(int) })]
// same with multiple rows:
[HarmonyPatch(typeof(TestClass))]
[HarmonyPatch(MethodType.Constructor)]
[HarmonyPatch(new Type[] { typeof(int) })]
Getters/Setters
To patch a property you use the annotations that contain a MethodType
argument and set it to MethodType.Getter
or MethodType.Setter
:
// in one row:
[HarmonyPatch(typeof(TestClass), "GameInstance", MethodType.Getter)]
// in two rows:
[HarmonyPatch(typeof(TestClass))]
[HarmonyPatch("GameInstance", MethodType.Getter)]
Generic Methods
To patch methods with generic signatures, you need to patch specific versions of the method. It is not possible to patch an open generic method. Example: AddItem(T item) cannot be patched directly but you can define one patch for i.e. AddItem(string item) and one for AddItem(int item):
[HarmonyPatch(typeof(TestClass<string>), "AddItem")]
Patching multiple methods
To simplify multiple patches while still using annotations, you can combine annotations with TargetMethod()
and TargetMethods()
:
[HarmonyPatch] // make sure Harmony inspects the class
class MyPatches
{
static IEnumerable<MethodBase> TargetMethods()
{
return AccessTools.GetTypesFromAssembly(someAssembly)
.SelectMany(type => type.GetMethods())
.Where(method => method.ReturnType != typeof(void) && method.Name.StartsWith("Player"))
.Cast<MethodBase>();
}
// prefix all methods in someAssembly with a non-void return type and beginning with "Player"
static void Prefix(object[] __args, MethodBase __originalMethod)
{
// use dynamic code to handle all method calls
var parameters = __originalMethod.GetParameters();
FileLog.Log($"Method {__originalMethod.FullDescription()}:");
for (var i = 0; i < __args.Length; i++)
FileLog.Log($"{parameters[i].Name} of type {parameters[i].ParameterType} is {__args[i]}");
}
}
Combining annotations
The combination of those annotations defines the target method. Annotations are inherited from class to method so you can use [HarmonyPatch(Type)]
on the class and [HarmonyPatch(String)]
on one of its methods to combine both.
using HarmonyLib;
[HarmonyPatch(typeof(SomeType))]
class MyPatches1
{
[HarmonyPostfix]
[HarmonyPatch("SomeMethod1")]
static void Postfix1() { }
[HarmonyPostfix]
[HarmonyPatch("SomeMethod2")]
static void Postfix2() { }
}
[HarmonyPatch(typeof(TypeA))]
class MyPatches2
{
[HarmonyPrefix]
[HarmonyPatch("SomeMethod1")]
static void Prefix1() { }
[HarmonyPrefix]
[HarmonyPatch("SomeMethod2")]
static void Prefix2() { }
[HarmonyPatch(typeof(TypeB), "SomeMethod1")]
static void Postfix() { }
}
[HarmonyPatch]
class MyPatches3
{
[HarmonyPatch(typeof(TypeA), "SomeMethod1")]
static void Prefix() { }
[HarmonyPatch(typeof(TypeB), "SomeMethod2")]
static void Postfix() { }
[HarmonyPatch(typeof(TypeC), "SomeMethod3")]
static void Finalizer() { }
}


Questionaire to help you choose your coding path.
Click to Begin
Front-end Design
Ruby
Click the image for more info.
Java/Android
Click the image for more info.
PHP and Drupal
Click the image for more info.
C# and .NET
Click the image for more info.


{% extends "partials/tooltips/base.html" %}
{% block title %}
Identification of Applicant (VSA 512)
{% endblock %}
{% block inner %}
This form is used by the Court to notify Vital Statistics of court-ordered legal changes of name.
This form requires you to complete it either by hand or using Adobe Acrobat Reader.
{% endblock %}
{% block label %}
{% if text %}{{ text }}{% else %}Identification of Applicant (VSA 512){% endif %}
{% endblock %}


Malik Ismail
32
min
Sits: 595A
Contact:<PHONE_NUMBER>
Hover
In Person
Monday
Tuesday
Wednesday
Thursday
Friday
In Car Experience
Stations
1010 AM
99.1 FM
92.5 FM
93.5 FM
104.5 FM
Conversation
Temperature
About
Sits
509b
Works
Finance
Savings
Carpooling with Malik
Action
Action
Another action
Something else here
Separated link
could save:
Money: $45
Money: $45
Money: $45


[April 6, 2020, Monday 05:00 AM. IST]
|
DnwsrI mhlw 5 ]
|
|
myrw lwgo rwm isau hyqu ] siqguru myrw sdw shweI ijin duK kw kwitAw kyqu ]1] rhwau ] hwQ dyie rwiKE Apunw kir ibrQw sgl imtweI ] inMdk ky muK kwly kIny jn kw Awip shweI ]1] swcw swihbu hoAw rKvwlw rwiK lIey kMiT lwie ] inrBau Bey sdw suK mwxy nwnk hir gux gwie]2]17] |
| somvwr, 24 cyq (sMmq 552 nwnkSwhI) | (AMg : 675) |
DnwsrI mhlw 5 ]hy BweI! ijs gurU ny srn Awey hryk mnu`K dw bodI vwlw qwrw hI sdw k`t id`qw hY(jyhVw gurU hryk srn Awey mnu`K dy du`KW dI jVH hI k`t dyNdw hY), auh gurU myrw BI sdw leI mddgwr bx igAw hY, qy aus dI ikrpw nwl myrw prmwqmw nwl ipAwr bx igAw hY[1[rhwau[ hy BweI! auh prmwqmw Awpxy syvkW nUM Awpxy h`Q dy ky du`KW qoN bcWdw hY, syvkW nUM Awpxy bxw ky auhnW dw swrw du`K-drd imtw dyNdw hY[ prmwqmw Awpxy syvkW dw Awp mddgwr bxdw hY, qy, auhnW dI inMdw krn vwilAW dy mUMh kwly krdw hY[1[ hy nwnk! sdw kwiem rihx vwlw mwlk Awpxy syvkW dw Awp rwKw bxdw hY, auhnW nUM Awpxy gl nwl lw ky r`Kdw hY[ prmwqmw dy syvk prmwqmw dy gux gw gw ky,qy, sdw Awqmk AwnMd mwx ky d`uKW klySW vloN infr ho jWdy hn[2[17[
DHANAASAREE, FIFTH MEHL:I have fallen in love with the Lord. My True Guru is always my help and support; He has torn down the banner of pain. || 1 || Pause || Giving me His hand, He has protected me as His own, and removed all my troubles. He has blackened the faces of the slanderers, and He Himself has become the help and support of His humble servant. || 1 || The True Lord and Master has become my Saviour; hugging me close in His embrace, He has saved me.


ROYAL BOTIQUE
HER SWEETNESS DRESS
€262.00
HER SWEETNESS DRESS
€262.00
HER SWEETNESS DRESS
€262.00
HER SWEETNESS DRESS
€262.00
HER SWEETNESS DRESS
€262.00
HER SWEETNESS DRESS
€262.00
SUMMER BREEZE
Longing for sun, sitting under summer light blue sky and sipping refreshing lemonade on the beach?
Choose your resort wardrobe for winter holiday escape in sun!
SHOP NOWAristocrat Kids Kingdom
Open this door and let the magic take you on a journey through our Royal Kingdom
DISCOVER


Nothing to see here, move along
It looks like the page you are trying to acces does not exist, this may be because it does not exist or something went wrong wth your browser or the server.
Here are some things you can do to fix this:
~Try
reloading the page.
~Check the spelling of the link.
~Contact the website admin(Noah Huppert).
~You might not be able to do anything, the page just might not exist.


Flow Contact Page
Main Navigation
Home
About
Contact
Mission Statment and Photo
Start your Journey Today.
Be radient, go with the flow.
Contact form
Contact Us Here.
Name: (required)
Email: (will not be published)
Phone: (required)
Comments:
What is 5 + 5?
Visit Us.
Flow Yoga Studio,
647 Richmond st. London, On
Phone:<PHONE_NUMBER>


Whenever one of the defined properties is set to a new value, Avers will generate a change
event and propagate it to the root. You can set up callbacks and listen for these changes.
The callback is called with two arguments: the path at which the change happened and a description
of the change.
The change operation is a JSON description of what was changed at that path. In the future
Avers will be able to undo individual operations.
var user = Avers.mk(User, {});
user.on('change', function(path, op) {
console.log('Change at path:', path);
});
user.name = 'Fry';
// A message should show up in the log:
// Change at path: name
In the near future, Avers will stop polluting the class prototype with its
own functions. Then you'll have to use Avers.on(obj, 'change', function(){})
to listen to changes.


This wsgi server is a single threaded, single process server that interleaves the iterations of the wsgi apps - I could add a threadpool for blocking apps in the future.
If you don’t return iterators from apps and return lists you’ll get, at most, the performance of a server that processes requests sequentialy.
On the other hand this server has coroutine extensions that suppose to support use of middleware in your application.
Example app with coroutine extensions:
def wait_app(environ, start_response):
start_response('200 OK', [('Content-type','text/html')])
yield "I'm waiting for some signal"
yield environ['cogen'].core.events.WaitForSignal("abc", timeout=1)
if isinstance(environ['cogen'].result, Exception):
yield "Your time is up !"
else:
yield "Someone signaled me: %s" % environ['cogen'].result
HTTP handling code taken from the CherryPy WSGI server.
Bases: object
An HTTP server for WSGI.
| Option | Description |
|---|---|
| bind_addr | The interface on which to listen for connections. For TCP sockets, a (host, port) tuple. Host values may be any IPv4 or IPv6 address, or any valid hostname. The string ‘localhost’ is a synonym for ‘<IP_ADDRESS>’ (or ‘::1’, if your hosts file prefers IPv6). The string ‘<IP_ADDRESS>’ is a special IPv4 entry meaning “any active interface” (INADDR_ANY), and ‘::’ is the similar IN6ADDR_ANY for IPv6. The empty string or None are not allowed. For UNIX sockets, supply the filename as a string. |
| wsgi_app | the WSGI ‘application callable’; multiple WSGI applications may be passed as (path_prefix, app) pairs. |
| server_name | the string to set for WSGI’s SERVER_NAME environ entry. Defaults to socket.gethostname(). |
| request_queue_size | the ‘backlog’ argument to socket.listen(); specifies the maximum number of queued connections (default 5). |
| protocol | the version string to write in the Status-Line of all HTTP responses. For example, “HTTP/1.1” (the default). This also limits the supported features used in the response. |
The interface on which to listen for connections.
For TCP sockets, a (host, port) tuple. Host values may be any IPv4 or IPv6 address, or any valid hostname. The string ‘localhost’ is a synonym for ‘<IP_ADDRESS>’ (or ‘::1’, if your hosts file prefers IPv6). The string ‘<IP_ADDRESS>’ is a special IPv4 entry meaning “any active interface” (INADDR_ANY), and ‘::’ is the similar IN6ADDR_ANY for IPv6. The empty string or None are not allowed.
For UNIX sockets, supply the filename as a string.
Bases: object
Server factory for paste.


Project Hedra is a roguelike game with RPG elements: open-world, replayable and quest-oriented are some of the features which best describe Project Hedra. The game is divided into "runs" where each world is procedurally generated and can vary in theme, appearance, natural complexity levels ( such as the variety of flora in the world and the weather ) along with many other factors which make each run a unique challenge.


SIGURD
Data Automation
Development
Servers and storage
Business solutions
Software Store
School
RUN A DATA DRIVEN BUSINESS
learn more
Let your Data boost Your Business Performance
find new customers
increase customer retention
improve customer service
Manage marketing efforts


Undocumented
Undocumented
SDLServiceTypeControl = 0x00
case control = 0
Undocumented
SDLServiceTypeRPC NS_SWIFT_NAME(rpc) = 0x07
case rpc = 7
Undocumented
SDLServiceTypeAudio = 0x0A
case audio = 10
Undocumented
SDLServiceTypeVideo = 0x0B
case video = 11
Undocumented
SDLServiceTypeBulkData = 0x0F
case bulkData = 15


This is an example of Dashboard usage with clickable "KPIs" (Key Performance Indicators) on the left and content wrapped in a split panel below. To view implementation details and other usage info, click the KPI items on the left.
The WufDashboardModule is comprised of two different components working together:
Both of these components are included as a part of the WufDashboardModule module from the @anviltech/wuf-ang-dashboard package in Artifactory.
Once installed, using the dashboard component is relatively simple. The <wuf-dashboard> itself has no attributes. Simply add it inside your page's <wuf-content-main> tag:
This will add the overall dashboard layout with a section on left to hold your KPIs and a section on the right to show the content for each KPI when that KPI is clicked.
However, you may notice a couple of things about the layout:
To solve both of these issues, add the following SCSS code to your page's *.component.scss
file:
The :host
section removes the content padding, allowing the dashboard to fill the entire
page space without any spacing around it.
The wuf-content-header
section causes the toolbar to float above the dashboard component,
allowing it to cast its dropshadow over the KPI section, which looks a little better and gives the sense
of depth that suggests the dashboard is a child of the toolbar (which it is).
Now that we have the dashboard framework in place, we can add some content to it. Dashboard content comes in the form of <wuf-kpi> components. To add content to a dashboard, place as many <wuf-kpi> tags inside the <wuf-dashboard> tag as you'd like:
The only required attributes for the <wuf-kpi> component are label and value.
When added, a new KPI will appear in the KPI section on the left displaying the label and value
provided. Additionally, the content you provided within the <wuf-kpi>
tags will be
shown on the right.
If you have added multiple <wuf-kpi>
tags to the parent
<wuf-dashboard>
tag, the <wuf-dashboard>
tag will ensure that only
one KPI will be active at a time and that only the contents of that active KPI will be displayed in the
content area. KPIs behave like tabs in this way and display their corresponding content only when
clicked and active. The first KPI added to the page is the initially active KPI on page load.
Notice that in the example to the left the "API" section displays a long string of 9 characters. In order
for the entire string to be visible, the <wuf-kpi>
tag is dynamically sizing the value
element based on string length. Additionally, the text size of the value will grow/shrink as the
available realestate within the browser grows/shrinks. It does this using a combination of SVG, CSS, and
some javascript. This mechanism ensures that KPI values can be displayed on as many different devices as
possible, including mobile devices where space is severely limited. The value can handle about
13 characters before it starts getting truncated.
| Property | Type | Default | Description |
|---|---|---|---|
| minKpiCount | number |
4 | Minimum number of KPIs to show. If the dashboard includes fewer than this number of <wuf-kpi> elements, filler KPIs will be added to match this number of displayed KPIs. Set to 0 to allow any number of KPIs. |
| Property | Type | Default | Description |
|---|---|---|---|
| color | string |
None | If added, this optional value will change the color of the right border. Any color name from the color palette (primary, secondary, accent, success, info, warning, danger) can be used here. This is a good way to indicate a KPI is in a state that requires user attention. |
| label | string |
None | The label to display in the KPI. Long strings will wrap. |
| padding | string |
20px | The amount of padding to display around content in the content area. Sometimes you may want to remove all padding in order to insert a split panel that doesn't need any padding. In this case you can pass any CSS size value here (e.g., px, em, rem, pt, etc.) |
| value | string|number |
None (required) | The value to display in the KPI. Values longer than about 13 characters in length will be cropped, depending upon available screen size and number of KPIs displayed. |
| CSS Custom property | Description | Value |
|---|---|---|
| --wuf-dashboard-content-padding | The CSS value for padding to use in the content area of the dashboard. | 20px |
| --kpi-border-color | The color for the line vertically separating the KPIs. | var(--wuf-kpi-border-color, var(--wuf-color-gray-400)) |
| --kpi-stripe-color | The color of the thick vertical line appearing on the right side of the KPI. | var(--wuf-kpi-stripe-color, var(--kpi-border-color)) |
| --kpi-label-color | The color of the label appearing above the KPI value. | var(--wuf-kpi-label-color, var(--wuf-color-gray-600)) |
| --kpi-bg-color | The background color of the KPI element. | var(--wuf-kpi-bg-color, var(--wuf-color-gray-200)) |
| --kpi-active-bg-color | The background color of the KPI element in an active state. | var(--wuf-kpi-active-bg-color, var(--wuf-color-primary-darker-5)) |
| --kpi-active-stripe-color | The stripe color to use for the KPI element in an active state. This color is overridden when the color property is used. |
var(--wuf-kpi-active-stripe-color, var(--wuf-color-primary-lighter-10)) |


Contact Me
I'm always looking for ways to improve. If you notice a problem with the website, do not hesitate to let me know in the form below. If you are interested in my services as a software developer, fill out the form below and I will be in contact with you shortly.


About Me
I am a researcher and graduate student in the DREAM Lab at UMass Amherst working with Gerome Miklau and Dan Sheldon. Before this, I was a Data Scientist at Allstate, an affiliate researcher at the Fiscal Research Center at Georgia State University, and studied mathematics and logic at Miami University in Oxford, Ohio.
Click here to view my CV.
You may contact me at brettcmullins(at)gmail.
This radio program on Frank Ramsey influenced my thinking and interests greatly.
Research Interests
Differential Privacy, Explainable Machine Learning, Learning Theory,
Causation, Formal Epistemology
My research involves using tools from mathematics, logic, and machine learning to approach a problem from a novel perspective.
See more about specific projects on my projects page.


Discount Calculator
Percent and discounts
Will your Luck give you a discount?
Well, let´s try it
This will calculate the price to pay for your products with discount
Put your product price:
Now, gimme the magic word
Split the price


1
2
1
2
Test
2
1
2
3
4
5
6
Test
2
Test
2
One
Two
Three
One
Two
Three
One
Two
Three
One
Two
Three
One
Two
One
2
One
2
One Two Three


Welcome back
Sign in to your account
Over 25,000 online stores use Cobiro - a free tool for Google Ads® - text and shopping ads. It’s an easy-to-use, intelligent advertising platform fully automating keyword planning and bidding.
Over 25,000 online stores use Cobiro - a free tool for Google Ads® - text and shopping ads. It’s an easy-to-use, intelligent advertising platform fully automating keyword planning and bidding.


JAEG: JPEG-Encoded Audio
Convert audio to image
Input audio:
Quality
Convert!
Convert image to audio
Input image:
Convert!


{# NOTE: Indenting here may look odd, but it is because this template is optimized for the user viewing HTML source on the page #} {% extends 'base.html' %} {% block header %} Showing all {{num_results}} recipes {% endblock %} {% block content %} {% if results|length > 0 %}
{{result.description|safe}}


Home
Download
Documentation
Community
Report a bug
Epigram 2 Community
Read the
Epigram blog
Chat in the #epigram irc channel on
FreeNode
Discuss Epigram on the
<EMAIL_ADDRESS>mailing list. Epigram, discuss.


VectorResolutionY()
Syntax
Result.d = VectorResolutionY()Description
Returns the vertical resolution of the vector drawing output area.
Parameters
None.
Return value
Returns the vertical resolution in DPI (dots per inch).
Remarks
The vertical resolution can differ from the horizontal resolution in the case of a printer output.
See Also
VectorResolutionX()
Supported OS
All


{% extends 'base.html' %} {% block nav_text_documents %}active{% endblock %} {% block header %}
Currently uploaded and tokenized text:
No text uploaded, yet.


Our mission is to offer an empowering and educational experience by providing an interactive platform that uses an advanced technological scanner to identify different species and elements while incorporating the cultural Hawaiian moʻolelo (stories). We believe that anyone who is interested in learning about the pae ʻāina (islands) of Hawaiʻi, should have an organized and community based space to help broaden their knowledge while keeping ancient wisdom and sustainability alive.
An empowered Hawaiʻi fluent in the language of aloha ʻāina, strengthened by the knowledge of our kūpuna (ancestors.)
“Lama,” meaning “light,” originates from the endemic Hawaiian plant used by the kūpuna (ancestors) of Hawaiʻi for ʻai (food), lāʻau (medication), and recreational practices such as holoholo (fishing) and hula (dance). The Lama tree is also associated with Laka; the Hawaiian goddess of dance, reproduction, and the forest.


1 2 3 4
5
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
37
38 /*!
39 * ======== gnu.targets.ITarget ========
40 * Interface to GCC compatible compilers
41 */
42 @TargetHeader("xdc/bld/stddefs.xdt")
43 metaonly interface ITarget inherits xdc.bld.ITarget3 {
44
45 override readonly config string stdInclude = "gnu/targets/std.h";
46 override config string dllExt = ".so";
47
48 /*!
49 * ======== GCCVERS ========
50 * Version number of the GCC compiler; e.g., "3.2".
51 *
52 * This string can be supplied by the user, otherwise it is obtained
53 * by running "gcc -dumpversion".
54 */
55 config string GCCVERS = null;
56
57 /*!
58 * ======== BINVERS ========
59 * Version number of binutils used with the compiler; e.g., "2.19".
60 *
61 * This string can be supplied by the user, otherwise it is obtained
62 * by running "ld -v".
63 */
64 config string BINVERS = null;
65
66 /*!
67 * ======== version ========
68 * The Compatibility Key associated with this target.
69 *
70 * The first two components of this target's Compatibility Key are '1,0'.
71 * The rest of the Key represents the compiler version. The third
72 * component combines the major and the minor version number in the format
73 * Major.Minor. The fourth component is the patch number.
74 *
75 * @a(Example)
76 * If this target's `rootDir` points to the compiler version 3.4.6, the
77 * Compatibility Key is [1,0,3.4,6].
78 *
79 */
80 override metaonly config String version;
81
82 /*!
83 * ======== GCCTARG ========
84 * The name of the platform executing programs produced by this target
85 *
86 * This string can be supplied by the user, otherwise is is obtained
87 * from the compiler and follows the GNU standard format
88 * (<cpu>-<manufacturer>-<os> or <cpu>-<manufacturer>-<kernel>-<os>);
89 * e.g., "arm-none-eabi" or "x86_64-unknown-linux-gnu".
90 *
91 * When building a GCC compiler, there are three different execution
92 * platforms to consider: the platform used to "build" the compiler, the
93 * "host" platform that runs the compiler, and the "target" platform
94 * that runs the executables produced by the compiler. All three
95 * platforms are identified using a
96 * {@link http://sources.redhat.com/autobook/autobook/autobook_17.html configuration name}
97 * defined by GNU Autotools. `GCCTARG` is the name of the "target"
98 * platform.
99 */
100 config string GCCTARG = null;
101
102 /*!
103 * ======== LONGNAME ========
104 * @_nodoc
105 * The "long name" of the gcc compiler
106 *
107 * This name is used (in conjunction with rootDir) to find the compiler
108 * and linker for this target. The format of `LONGNAME` is always
109 * "/bin/<machine>-gcc". For majority of the targets, the default value
110 * for `LONGNAME` does not ever need to be changed. But, there are
111 * targets where the different but compatible compilers may have
112 * different `LONGNAME` parameters. For such targets and compilers,
113 * `LONGNAME` can be set in `config.bld`.
114 *
115 * @a(Example)
116 * If a version 2010q1 of the CodeSourcery GNU toolchain for Arm is
117 * installed in C:/CodeSourcery/arm-2010q1, the following settings in
118 * `config.bld` configure `gnu.targets.arm.GCArmv6` target to use that
119 * toolchain:
120 * @p(code)
121 * var GCArmv6 = xdc.module("gnu.targets.arm.GCArmv6");
122 * GCArmv6.rootDir = "C:/CodeSourcery/arm-2010q1";
123 * GCArmv6.LONGNAME = "bin/arm-none-linux-gnueabi-gcc";
124 * @p
125 *
126 */
127 config string LONGNAME = null;
128
129 /*!
130 * ======== CYGWIN ========
131 * Is the target's compiler a cygwin executable
132 *
133 * Since file names produced by cygwin-based tools differ from the
134 * names understood by other Windows executables, it is important
135 * to avoid using the names output by cygwin tools as input to
136 * non-cygwin programs. This property tells the target whether
137 * or not it's possible to use the output from `gcc -MD -MF`, for
138 * example.
139 */
140 readonly config Bool CYGWIN = false;
141
142 /*!
143 * ======== noStdLinkScript ========
144 * Don't use the standard linker script
145 *
146 * If `true`, add a `-T` flag before the generated `package/cfg/*.xdl`
147 * file passed to the linker. This flag suppresses use of the
148 * standard linker script implicit in the GCC flow, which effectively
149 * says the generated `.xdl` file assumes total control for all
150 * `MEMORY` and `SECTION` directives.
151 *
152 */
153 config Bool noStdLinkScript = false;
154
155 156 157
158 override config xdc.bld.ITarget.OptionSet profiles[string] = [
159 ["debug", {
160 compileOpts: {
161 copts: "-g",
162 defs: "-D_DEBUG_=1",
163 },
164 linkOpts: "-g",
165 }],
166
167 ["release", {
168 compileOpts: {
169 copts: "-O2 -ffunction-sections -fdata-sections",
170 },
171 linkOpts: "-Wl,--gc-sections",
172 }],
173
174 ["profile", {
175 compileOpts: {
176 copts: "-g -pg",
177 },
178 linkOpts: "-pg"
179 }],
180
181 ["coverage", {
182 compileOpts: {
183 copts: "-fprofile-arcs -ftest-coverage",
184 },
185 linkOpts: "-fprofile-arcs -ftest-coverage",
186 }],
187 ];
188
189 /*!
190 * ======== versionMap ========
191 * Map of GCC compiler version numbers to compatibility keys.
192 *
193 * This map translates version string information from the compiler
194 * into a compatibility key. The compatibilty key is used to
195 * validate consistency among a collection of packages used in
196 * a configuration.
197 *
198 * The compiler version string is "gcc<ver>", where <ver> is
199 * GCCVERS.
200 *
201 * If a compiler version is not found in this map the default is
202 * "1,0,<ver>", where <ver> is the compiler version number. Thus,
203 * the user only needs to extend this table when a significant
204 * incompatibility occurs or when two versions of the compiler should
205 * be treated as 100% compatible.
206 */
207 override config string versionMap[string] = [
208 ["gcc3.2", "1,0,3.2,0"],
209 ];
210
211 /*!
212 * ======== remoteHost ========
213 * Remote host used to run compiler, linker, and archiver tools
214 *
215 * If `remoteHost` is `null` (or `undefined`), the configured compiler
216 * is run locally; otherwise, `remoteHost` is taken to be the host name
217 * of the machine that that should be used to run the specified compiler.
218 *
219 * All target commands are prefixed with a command that uses `rsh` to run
220 * the commands on the specified host. Thus, in order to use this
221 * setting, the remote machine must be support `rsh` and the user must
222 * have permission to run commands from the local machine on the remote
223 * host named `remoteHost`. This usually involves adding a line to the
224 * user's `~/.rhosts` file on the remote machine of the form:
225 * @p(code)
226 * local-machine-name user-name
227 * @p
228 * where `local-machine-name` is the name of the local machine and
229 * `user-name` is the user's login name on the local machine.
230 */
231 config string remoteHost;
232
233 /*!
234 * ======== ar ========
235 * The command used to create an archive
236 */
237 override readonly config xdc.bld.ITarget2.Command ar = {
238 cmd: "$(rootDir)/bin/ar",
239 opts: "cr"
240 };
241
242 /*!
243 * ======== lnk ========
244 * The command used to link executables.
245 */
246 override readonly config xdc.bld.ITarget2.Command lnk = {
247 cmd: "$(rootDir)/bin/gcc",
248 opts: ""
249 };
250
251 override config xdc.bld.ITarget2.Options lnkOpts = {
252 prefix: "",
253 suffix<EMAIL_ADDRESS>-lstdc++ -L$(rootDir)/lib"
254 };
255
256 /*!
257 * ======== cc ========
258 * The command used to compile C/C++ source files into object files
259 */
260 override readonly config xdc.bld.ITarget2.Command cc = {
261 cmd: "$(rootDir)/bin/gcc -c -MD -MF<EMAIL_ADDRESS>262 opts: ""
263 };
264
265 /*!
266 * ======== asm ========
267 * The command used to assembles assembly source files into object files
268 */
269 override readonly config xdc.bld.ITarget2.Command asm = {
270 cmd: "$(rootDir)/bin/gcc -c -x assembler",
271 opts: ""
272 };
273
274 /*!
275 * ======== includeOpts ========
276 * Additional user configurable target-specific include path options
277 */
278 override config string includeOpts = "";
279
280 override config String binaryParser = "xdc.targets.omf.Elf";
281
282 283 284 285
286 String initVers();
287
288 /*!
289 * ======== asmName ========
290 * The function that converts a C name into an assembly name
291 */
292 String asmName(String CName);
293
294 /*!
295 * ======== bspLib ========
296 * bspLib is assigned the name of the BSP library. The specified library
297 * is included on the link line.
298 */
299 config string bspLib = null;
300 }
301 302 303 304
305


From:ETS General Announcement/ET&S/Enron@ENRON To:Enron Transportation Services Everyone@ENRON Sent:2017-01-11T04:38:08.0000000Z Subject:Organizational Announcement
I am pleased to announce that Jana Domke has accepted the position of Director, Compensation for Enron Transportation Services, effective August 1, 2001.
Jana started with Enron in May, 2000 and most recently has been Director of Compensation & Benefits for Enron Wind. Prior to joining Enron, Jana was a Practice Leader with PricewaterhouseCoopers, and Director, International Compensation & Benefits for Smith International. Jana has 19 years of experience in both domestic and international compensation and benefits.
Jana received her M.B.A. from the University of Houston. She also has a Bachelors Degree from U of H in Organizational Behavior & Management.
Jana can be reached at<PHONE_NUMBER> and her office location is EB1156. The ETS Compensation staff, including Jana's direct reports, can be viewed on the attached organization chart.
Please join me in welcoming Jana to the ETS team.
***********
EDRM Enron Email Data Set has been produced in EML, PST and NSF format by ZL Technologies, Inc. This Data Set is licensed under a Creative Commons Attribution 3.0 United States License <http://creativecommons.org/licenses/by/3.0/us/> . To provide attribution, please cite to "ZL Technologies, Inc. (http://www.zlti.com)."
***********
California


{{model.Definition}}
Observation units Observation units are objects that are subject to particular instances of observation and measurement. An observation unit comprises one or more plants, and their environment. Synonym : Experimental unit.
Let's add a new observation unit!
Click on DONE to add a 10 observations units, one for each plot, plot were grouped by experimental factor value, (5 rainfed plots and 5 watered plots), called plot_1-10 with the following values:
The other fields can be fullfilled later


Fun Programs for Kids
Are you a young person looking to learn more about science? Come on down to our museum, there’s plenty to see and do. You can learn about Newtonian physics from our bumper swing, or why not travel back in time and meet our resident Woolly Mammoth? Our exhibits are designed to be accessible for interested minds, so make sure you come ready to learn and explore.
Read More


In this guide we'll show you how to develop a Vert.x project using Gradle.
We provide a template Gradle project which you can clone to get you started.
Clone it locally
git clone https://github.com/vert-x/vertx-gradle-template.git my-vertx-module
Where my-vertx-module
is the name you want to give your project.
Remove the origin
git remote rm origin
And add your new origin
git remote add origin <path to your repo>
Let's run the tests to make sure everything is working
cd my-vertx-module ./gradlew test
You should use the Gradle Wrapper (./gradlew
) to run all Gradle tasks. You do not need to install Gradle manually. Take a look at build.gradle
for a list of the available tasks.
The outputs of the project are:
The outputs are created in the build
directory as per normal.
You configure many things in gradle.properties
:
modowner
, modname
and version
determine the name of the module as described in the modules manual
pullInDeps
determines whether all module dependencies should be packaged into the module as nested modules.
It also contains various properties used to configure versions of various dependencies.
If you want to override any Vert.x platform configuration, e.g. langs.properties
, cluster.xml
or logging configuration, you can add those files to the directory src/main/platform_lib
- these will then be added to the Vert.x platform classpath when you run the module with ./gradlew runMod
Open build.gradle
and take a look at the comments there for a list of useful tasks supported by the build script.
You can use the idea
and eclipse
Gradle plugins to create the project files for your IDE
./gradlew idea
Or
./gradlew eclipse
Once the IDE files have been created you can open the project files in your IDE.
Note: You can run the idea
or eclipse
tasks again if you change your project dependencies - in this way the IDE project files will be brought up-to-date.
You may have to tell your IDE to use Java source compatibility level of Java 7, as Gradle seems to default to Java 6 (!)
If your project needs a third party jar to build and you want to include it in the lib
directory of your module you can add the dependency in the dependencies
section of build.gradle
with a type of compile
.
If you don't want it to be included in the lib
directory you should add it as provided
.
Once you've changed your dependencies just run ./gradlew idea
or ./gradlew eclipse
again to update your IDE project files with the new dependencies.
Use ./gradlew install
to install your module in your local Maven repository.
Use ./gradlew uploadArchives
as normal to push your module to a Maven repository.
If you've pushed your module to a public Maven or Bintray repository you can register it in the Module Registry so others can search for and discover it.
Now you've got the project all set-up and running, it's time to explore the standard project layout itself.


FluScores
Select zip files below. You can compare different teams by selecting multiple files.
All processing is done locally in your web browser; no data is sent to the server.
Season: |
|
Fluscores has been developed and tested under Chrome. Other browsers may or may not work for now.
FluScores


WITNESS LIST State Affairs Committee February 18, 1997-1:30P SB 237 On: Bennett, Ridgely (TX Lottery Commission), Austin SB 238 On: Bennett, Ridgely (TX Lottery Commission), Austin SB 343 For: Hoelzer, David (Self), Port Neches On: Griebel, Tom (TX Dot), Austin Registering, but not testifying: For: Taylor, Des (TX Rec. Vehicle Assn.), Austin Thompson, Jamie (TX Rec. Vehicle Assn.), Austin SB 438 Registering, but not testifying: On: Braddus, Jim (Dir.Facilities Plan,UT), Austin Cunningham, William (Chancellor, UT), Austin Royal, Darrell K. (Asst. to Pres. UT), Austin


You may select a picture and mask by clicking on it. the resulting image is shown at the bottom.
All masks on this page were obtained at
http://psp-pals.com/
Resulting image (after a pic and mask have been combined)


Welcome to securethatjob, the only internet based recruitment and networking platform specialised for the Security Industry. You will be part of a revolutionary new approach into receiving work, even if it’s at the last minute…
Our vision is to provide a specialised symbiotic website dedicated to the Security Industry. By providing an online marketplace to improve the access for people in the industry to get the best jobs available and for clients to access the best possible candidate for the job nationally.
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam convallis neque sit amet lacinia volutpat. Donec accumsan lectus maximus sagittis euismod. Donec lobortis volutpat erat at feugiat. Ut ut eros consectetur, consequat nibh ut, elementum justo. Sed sed est eu nisi gravida venenatis. In aliquam feugiat elit, eu commodo nunc lobortis sit amet.
Sed interdum neque quis dui gravida, at tristique tortor condimentum. Aenean vel condimentum libero. Cras venenatis a mauris et varius. Aenean maximus nunc in augue elementum aliquam.
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi pellentesque purus nec bibendum malesuada.
Learn moreLorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi pellentesque purus nec bibendum malesuada.
Learn more


{% extends "base.html" %} {% block content %}
{{stats|length}} patches by {{submitters|length}} submitters
{{submitter[0]['username']}} / submitted {{submitter|length}} patches
{{submitter[0]['country']}}


Changelog¶
All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog.
1.7.1 - 2021-05-14¶
New features:¶
Add equilibrationRotationRange, equilibrationTranslationRange and equilibrationBoxRadius parameters to tune equilibration performance
Add support to correctly run simulations with PELE interstep reports and trajectories
Bug fixes:¶
Fix bug reading the ligand information in the adaptiveSampling main, which caused to set the equilibration box in the center of mass of the whole system
1.7 - 2021-02-11¶
New features:¶
Use residue numbers and chain names in clustering, which makes possible to run protein-protein simulations
The plotAdaptive script now accepts a path to the simulation folder and has an option to skip the first step, or a number of steps when plotting
Bug fixes:¶
Fix bugs running MD simulations without ligand after the changes in previous version
1.6.3 - 2020-09-28¶
New features:¶
Add annotations to plotAdaptive, which show the origin (epoch, trajectory and snapshot) of the plot points
Parametrize more than one ligand in MD simulations
Include confactors in MD simulations
MD simulations can now be extended in time
Bug fixes:¶
Fix bug ignoring ligandName parameter in the simulation block
Behaviour changes from previous version:¶
Modify plotAdaptive to generate the plots using matplotlib and not rely on gnuplot
Raise separate and more informative errors for the cases of input file not existing, resname selection incorrect, input file in text file but not pdb and topology mismatching for binary files
Constrain the heavy atoms in the minimization run at the begging of the epochs in MD simulation, to preserve similiraty with the original cluster
1.6.2 - 2019-07-24¶
New features:¶
Add possibility to generate cylinder box from pdb
Add coordinate wrapping to XTC reporter
Bug fixes:¶
Fix bug restarting MD simulation with constraints
Fix bug that crashed when constraining HIS
Fix colorbar range for plotAdaptive script
Fix bug in HIS protonation
Behaviour changes from previous version:¶
Allow PELE equilibration to run without a box
Read PELE and MD reports seemingly
Add postprocessing option to simulationRunner
Add proper topology support to selectOnPlot and backtrackAdaptiveTrajectory
Write topologies.pkl at the start of the first epoch
1.6.1 - 2019-04-26¶
New features:¶
Add cylindrical box for MD
Add script to generate cylindrical box for visualization
Introduce new postprocessing function for MD
Bug fixes:¶
Fix bug selecting topolgies for odd number of initial conditions
Fix bug extracting indexes from topology in MSMClustering
Fix bug in atomset writing PDBs with gaps, now if there are residues with a difference in more than one in the residue number a TER is written
Behaviour changes from previous version:¶
Now the MSMClustering with PELE simulation repeats the rejected steps
1.6 - 2019-02-19¶
New features:¶
Add the possibility of running MD simulations using OpenMM
Add new script analysis/identifyClusterSnapshot.py, to identify to which cluster belongs a given conformation within a simulation
Add support for formats trr, dcd and dtr, mdcrd, nc
Add the null clustering method
Add independentMetric spawning
Add MSM-based spawning methods
Add reportName template for PELE control file
Bug fixes:¶
Fix bug in PELE equilibration when number of initial structures selected exceeded number of processors
Fix bug in atomset that wrote MODEL lines in PDBs non-compliant with the standard
Fix minor bug in in select equilibration structure with trajectories with no accepted steps
Behaviour changes from previous version:¶
Restructured a good part of the code in the adaptiveSampling main referring to simulation, moved into SimulationRunner class
Change how AdaptivePELE deals with topologies, now it supports several different topologies in a single simulation
Change how the spawning parameters are used, now are an attribute of the spawning calculator
Update how the srun command is called when running PELE, also added srunParameters to customize the call to srun
AdaptivePELE now runs with replicas synchronized via files, needed for running MD in GPU clusters
1.5.2 - 2018-08-13¶
New features:¶
AdaptivePELE can now be installed through pip
Bug fixes:¶
Fix bug in setup.py in environments without cython
1.5.1 - 2018-06-07¶
New features:¶
The extractCoords script now works seemesly with pdb or xtc trajectories
Behaviour changes from previous version:¶
Improve the speed of handling xtc trajectories by switching to the low-level API of mdtraj
Optimize and parallelize extractCoords script from the freeEnergies subpackage, change the multiprocess module to multiprocessing
Bug fixes:¶
Fix several bugs in extractCoords script
1.5 - 2018-05-11¶
New features:¶
Make code compatible with python2 and python3
Add posibility of using a third column as color in plotAdaptive
Add __version__ attribute to package
Add possibility of skipping first structure of each trajectory in clustering when calling cluster function
Add compatibility with non-pdb trajectories
Behaviour changes from previous version:¶
Change rmsd and be otions of plotAdaptive to lines and points
Change name of writePrecisePathToSnapshots to bactrackAdaptiveTrajectory, added name parameter to select the name of the output file and automatic detection of said name, so that if a file exists with the same name, a number is added at the end to differentiate them
Optimize and parallelize extractCoords script from the freeEnergies subpackage
Bug fixes:¶
Fix bug in alternative structure when a cluster had no other structure than the representative
Fix several bugs related to unicode and string handling
1.4.2 - 2018-03-02¶
New features:¶
Added null spawning calculator
Added possibility of max metric in epsilon
Behaviour changes from previous version:¶
Improvements in REAP spawning
Metric columns in control file now start by 1
Changed symbolic links in rawData in freeEnergies calculation to relative paths
Bug fixes:¶
Various bug fixes
1.4 - 2018-01-30¶
New features:¶
Added scripts plot3DNetwork, plotSpawningClusters for better visualization of simulations
Added exitContinuous density for exit path simulations
Added possibility to change the simulation box at each epoch
Added equilibration procedure
Added possibility to test metric greater than in metric exit condition
Added metricMultipleTrajectories exit condition
Behaviour changes from previous version:¶
Moved buildRevTransitionMatrixFunction to Cython code (speed-up of up to 500x)
Bug fixes:¶
Fixed minor bug in controlFileValidator
Fixed bug in writePrecisePathToSnapshot, where backtracking was not carried out until the initial structure
1.3 - 2017-06-01¶
New features:¶
Added script to reconstruct precise path to a given snapshot (writePrecisePathToSnapshot.py)
Added possibility of chain and resnum selection in PDB
Added scripts to calculate free energies in pyemma_scripts
Added new parameter to control the number of clusters considered in epsilon scoring
Behaviour changes from previous version:¶
Change names of clustering in control file
Bug fixes:¶
Minor bug fixes in scripts to calculate free energies
Fixed bug of incorrect trajectory selection in estimateDG
Fixed bug of multiple its plot not visible (bug due to pyemma)
1.2 - 2017-05-09¶
New features:¶
Added conformation network and first discovery tree to improve simulation analysis
Added scripts to plot RMSF for each residue over a trajectory
Added scripts to calculate contact map histogram for each residue over a trajectory or a complete simulation
Added scripts to create a network of residues over a trajectory or a complete simulation
Added more robust pickling interface so old simulation can be used with newer version (to some extent)
Added script to reconstruct approximate path to a given snapshot (writeTrajToSnapshot.py)
Behaviour changes from previous version:¶
Alternative structures are stored in a priority queue with the priority set to the population of the subclusters spawn inversely proportinal way according to this population
Bug fixes:¶
Fix bug in spawning of alternative structures, was not calling the new code for randomly spawn from cluster center of alternative structure
Fix bug in pickling (serializing) coordinates of Atom objects
Fix bug in pickling AltStructures objects
1.1 - 2017-02-17¶
New features:¶
Follow proper packaging conventions for Python packaging
Added alternative structure to each cluster that will spawn 50% of the time
Implemented UCB algorithm for spawning
Behaviour changes from previous version:¶
Atomset package implemented in Cython (faster)
Jaccard index is calcualed using only the cells of the matrix that are 1
1.0 - 2017-01-19¶
New features:¶
Added support for symmetry with contactMap
Added lastSnapshot clustering for easy restart of sequential runs
Added independent spawning to perform classical PELE simulations
Added exitCondition on metric
Added support for changing clustering when clustering method parameter changes, and be able to handle metric column change in spawning
Added suport for wildcard in control file input structures
Added several scripts for analysis
Behaviour changes from previous version:¶
Changed quadratic function for continuous
Changed symmetry dictionary for list of dictionaries, with symmetry groups
Bug fixes:¶
Fixed bug of incorrect atom consideration in symmetries
Fixed bug of NaN correlation similarity evaluator in contactMap


Installation of WPA Supplicant
First you will need to create an initial configuration file for the
build process. You can read wpa_supplicant/README
and wpa_supplicant/defconfig
for the explanation of
the following options as well as other options that can be used.
Create a build configuration file that should work for standard
WiFi setups by running the following command:
cat > wpa_supplicant/.config << "EOF"
CONFIG_BACKEND=file
CONFIG_CTRL_IFACE=y
CONFIG_DEBUG_FILE=y
CONFIG_DEBUG_SYSLOG=y
CONFIG_DEBUG_SYSLOG_FACILITY=LOG_DAEMON
CONFIG_DRIVER_NL80211=y
CONFIG_DRIVER_WEXT=y
CONFIG_DRIVER_WIRED=y
CONFIG_EAP_GTC=y
CONFIG_EAP_LEAP=y
CONFIG_EAP_MD5=y
CONFIG_EAP_MSCHAPV2=y
CONFIG_EAP_OTP=y
CONFIG_EAP_PEAP=y
CONFIG_EAP_TLS=y
CONFIG_EAP_TTLS=y
CONFIG_IEEE8021X_EAPOL=y
CONFIG_IPV6=y
CONFIG_LIBNL32=y
CONFIG_PEERKEY=y
CONFIG_PKCS12=y
CONFIG_READLINE=y
CONFIG_SMARTCARD=y
CONFIG_WPS=y
CFLAGS += -I/usr/include/libnl3
EOF
If you wish to use WPA Supplicant
with NetworkManager-<IP_ADDRESS>, add the
required options to the WPA
Supplicant build configuration file by running the following
command:
cat >> wpa_supplicant/.config << "EOF"
CONFIG_CTRL_IFACE_DBUS=y
CONFIG_CTRL_IFACE_DBUS_NEW=y
CONFIG_CTRL_IFACE_DBUS_INTRO=y
EOF
First, fix expand the list of parameters that are passed to the
wpa_supplicant when
started as a D-Bus service:
sed -e "s@wpa_supplicant -u@& -s -O /var/run/wpa_supplicant@g" -i wpa_supplicant/dbus/*.service.in &&
sed -e "s@wpa_supplicant -u@& -s -O /var/run/wpa_supplicant@g" -i wpa_supplicant/systemd/wpa_supplicant.service.in
Install WPA Supplicant by running
the following commands:
cd wpa_supplicant &&
make BINDIR=/sbin LIBDIR=/lib
If you have installed Qt-4.8.6 and wish to build the WPA Supplicant GUI program, run the following
commands:
pushd wpa_gui-qt4 &&
qmake-qt4 wpa_gui.pro &&
make &&
popd
This package does not come with a test suite.
Now, as the root
user:
install -v -m755 wpa_{cli,passphrase,supplicant} /sbin/ &&
install -v -m644 doc/docbook/wpa_supplicant.conf.5 /usr/share/man/man5/ &&
install -v -m644 doc/docbook/wpa_{cli,passphrase,supplicant}.8 /usr/share/man/man8/
Install the systemd support files
by running the following command as the root
user:
install -v -m644 systemd/*.service /lib/systemd/system/
If you have built WPA Supplicant
with D-Bus support, you will need
to install D-Bus configuration
files. Install them by running the following commands as the
root
user:
install -v -m644 dbus/fi.{epitest.hostap.WPASupplicant,w1.wpa_supplicant1}.service \
/usr/share/dbus-1/system-services/ &&
install -v -m644 dbus/dbus-wpa_supplicant.conf \
/etc/dbus-1/system.d/wpa_supplicant.conf
Additionally, enable the wpa_supplicant.service
so that systemd can properly activate the D-Bus service. Run the following command as
the root
user:
systemctl enable wpa_supplicant
If you have built the WPA
Supplicant GUI program, install it by running the following
commands as the root
user:
install -v -m755 wpa_gui-qt4/wpa_gui /usr/bin/ &&
install -v -m644 doc/docbook/wpa_gui.8 /usr/share/man/man8/ &&
install -v -m644 wpa_gui-qt4/wpa_gui.desktop /usr/share/applications/ &&
install -v -m644 wpa_gui-qt4/icons/wpa_gui.svg /usr/share/pixmaps/
Note
You will need to restart the system D-Bus daemon before you can use the
WPA Supplicant D-Bus interface.
Note
This package installs desktop files into the /usr/share/applications
hierarchy and you can
improve system performance and memory usage by updating
/usr/share/applications/mimeinfo.cache
. To
perform the update you must have desktop-file-utils-0.22 installed
and issue the following command as the root
user:
update-desktop-database
Configuring wpa_supplicant
Config File
/etc/wpa_supplicant/wpa_supplicant-*.conf
Configuration Information
Warning
You need to replace wlan0
with the correct wireless
interface name in the commands below.
To connect to an access point that uses a password, you need to
put the pre-shared key in /etc/wpa_supplicant/wpa_supplicant-wlan0
.conf
. SSID is the
string that the access point/router transmits to identify itself.
Run the following command as the root
user:
install -v -dm755 /etc/wpa_supplicant &&
wpa_passphrase SSID
SECRET_PASSWORD
> /etc/wpa_supplicant/wpa_supplicant-wlan0
.conf
/etc/wpa_supplicant/wpa_supplicant-wlan0
.conf
can hold the
details of several access points. When wpa_supplicant is started, it
will scan for the SSIDs it can see and choose the appropriate
password to connect.
If you want to connect to an access point that isn't password
protected, put an entry like this in /etc/wpa_supplicant/wpa_supplicant-wlan0
.conf
. Replace
"Some-SSID" with the SSID of the access point/router.
network={
ssid="Some-SSID
"
key_mgmt=NONE
}
There are many options that you could use to tweak how you
connect to each access point. They are described in some detail
in the wpa_supplicant/wpa_supplicant.conf
file in the
source tree.
Connecting to an Access Point
There are 3 types of systemd
units that were installed:
The only difference between 3 of them is what driver is used for
connecting (-D option). The first one uses the default driver,
the second one uses the nl80211 driver and the third one uses the
wired driver.
You can connect to the wireless access point by running the
following command as the root
user:
systemctl start wpa_supplicant@wlan0
To connect to the wireless access point at boot, simply enable
the appropriate wpa_supplicant service by
running the following command as the root
user:
systemctl enable wpa_supplicant@wlan0
Depending on your setup, you can replace the<EMAIL_ADDRESS>with any other listed
above.
To assign a network address to your wireless interface, consult
the General
Network Configuration page in LFS.


BJP-Sena should hold CM's post; suggests Ramdas Athawale
Athawale had earlier stated that Maharashtra would soon see an NDA government.
by ANINew Delhi: Union Minister and Republican Party of India (A) chief Ramdas Athawale on Monday said that the Bharatiya Janata Party (BJP) and the Shiv Sena should form the government in Maharashtra and can have their CM for three years and two years respectively.
Speaking to ANI in Parliament, Athawale said: "I met Sanjay Raut (Shiv Sena leader) and urged him to ponder over a formula of having a chief minister from the BJP for three years, and from the Sena for remaining two years."
Athawale added that Raut then asked him to speak with the BJP regarding the formula he was suggesting to the Shiv Sena.
Athawale had earlier stated that Maharashtra would soon see an NDA government.
"I told Amit Bhai (BJP president Amit Shah) that if he mediates, then a way can be found out to which he (Amit Shah) replied, don't worry, everything will be fine. BJP and Shiv Sena will come together to form the government."
Maharashtra came under the President's Rule last week after all the parties failed to form a government in the state.
BJP, which emerged as the single largest party, could not stake claim to form a government as its ally Shiv Sena remained firm on rotating the Chief Minister's post and equal sharing of Cabinet berths.
Shiv Sena parted its ways with the BJP to explore ways to form a government. It, however, failed to prove the support of the required number of MLAs in the time given by Governor Bhagat Singh Koshyari.
The Governor had then invited NCP, the third-largest party, to show its willingness to form the government, failing which the President's Rule was imposed in the state on last Tuesday.
The Shiv Sena is now in talks with the Congress and the NCP to form a government in the state.
The BJP won 105 seats in the 288-member assembly followed by Shiv Sena 56, NCP 54 and Congress 44. The majority mark in the 288-member Maharashtra assembly is 145.
Catch the latest news, live coverage and in-depth analyses from India and World. Follow us on Facebook and Twitter.


Bangladesh pacer Abu Jayed takes tips from Mohammed Shami, hopes to bowl like him
by Renin Wilben AlbertTeam India pacer Mohammed Shami was brilliant in the Indore Test against Bangladesh, picking up 3 for 27 and 4 for 31 as India won the Test by an innings and 130 runs to go 1-0 up. Bangladesh pacer Abu Jayed, who was among the few bright spots for the visitors with four wickets, feels that he can learn a lot from Shami.
Jayed believes that there are similarities between him and the Indian pacer since both use the seam of the ball. He even took tips from Shami with an aim to improve his bowling.
"I spoke with Shami bhai yesterday (Saturday). There are some similarities between him and me since we both use the seam. I have seen him bowl a lot of times and I paid extra attention to how he was bowling," Abu Jayed was quoted as saying in a report on the ICC website.
"I have compared his height to mine to find out if he is taller than me or of equal height. Then I figured maybe I could bowl like him," Jayed added.
Jayed shone amid the ruins at Indore, picking up the first four Indian wickets to fall. He dismissed Rohit Sharma (6), Cheteshwar Pujara (54), Virat Kohli (0) and Ajinkya Rahane (86) to finish with figures of 4 for 108 in 25 overs.
Jayed is relatively new to Test cricket. Having made his debut against West Indies last year, he has so far played six Tests with 15 wickets at an average of 36.06 and a best of 4 for 59. In addition, he has played two ODIs and picked up 5 for 58 in his second game, a match against Ireland.
Coming back to the India-Bangladesh Test series, the teams will next face each other in the second game at the Eden Gardens in Kolkata, starting from November 22. This will be the first ever day-night Test match in India.


In this example, we fill holes (i.e. isolated, dark spots) in an image using morphological reconstruction by erosion. Erosion expands the minimal values of the seed image until it encounters a mask image. Thus, the seed image and mask image represent the maximum and minimum possible values of the reconstructed image.
We start with an image containing both peaks and holes:
import matplotlib.pyplot as plt
from skimage import data
from skimage.exposure import rescale_intensity
image = data.moon()
# Rescale image intensity so that we can see dim features.
image = rescale_intensity(image, in_range=(50, 200))
# convenience function for plotting images
def imshow(image, **kwargs):
plt.figure(figsize=(5, 4))
plt.imshow(image, **kwargs)
plt.axis('off')
imshow(image)
plt.title('original image')
Now we need to create the seed image, where the minima represent the starting points for erosion. To fill holes, we initialize the seed image to the maximum value of the original image. Along the borders, however, we use the original values of the image. These border pixels will be the starting points for the erosion process. We then limit the erosion by setting the mask to the values of the original image.
import numpy as np
from skimage.morphology import reconstruction
seed = np.copy(image)
seed[1:-1, 1:-1] = image.max()
mask = image
filled = reconstruction(seed, mask, method='erosion')
imshow(filled, vmin=image.min(), vmax=image.max())
plt.title('after filling holes')
As shown above, eroding inward from the edges removes holes, since (by definition) holes are surrounded by pixels of brighter value. Finally, we can isolate the dark regions by subtracting the reconstructed image from the original image.
imshow(image - filled)
plt.title('holes')
Alternatively, we can find bright spots in an image using morphological reconstruction by dilation. Dilation is the inverse of erosion and expands the maximal values of the seed image until it encounters a mask image. Since this is an inverse operation, we initialize the seed image to the minimum image intensity instead of the maximum. The remainder of the process is the same.
seed = np.copy(image)
seed[1:-1, 1:-1] = image.min()
rec = reconstruction(seed, mask, method='dilation')
imshow(image - rec)
plt.title('peaks')
plt.show()
Python source code: download (generated using skimage 0.9.0)


It’s possible to create functions in JavaScript using the Function
constructor, such as:
var x = new Function("a", "b", "return a + b");
This is considered by many to be a bad practice due to the difficulty in debugging and reading these types of functions.
This error is raised to highlight the use of a bad practice. By passing a string to the Function constructor, you are requiring the engine to parse that string much in the way it has to when you call the eval
function.
Examples of incorrect code for this rule:
/*eslint no-new-func: "error"*/
var x = new Function("a", "b", "return a + b");
var x = Function("a", "b", "return a + b");
Examples of correct code for this rule:
/*eslint no-new-func: "error"*/
var x = function (a, b) {
return a + b;
};
In more advanced cases where you really need to use the Function
constructor.
This rule was introduced in ESLint 0.0.7.


(Colors shown above L to R): BULLHIDE BROWN, BULLHIDE NATURAL, and BULLHIDE BLACK.
|
(Stamps shown above L to R): GREAT SEAL OF THE USA and SCOTTISH THISTLE.
|
(Shown above L to R): HORSE HIDE NATURAL WITH NO STAMP, SKULL AND CROSS BONES, BELTMAN LOGO, JUMPING BASS, AND CELTIC CROSS.
* Pint sleeves ship FREE if ordered WITH a belt.
We DO NOT ship pint sleeves overseas unless you are ordering them WITH a belt.
If ordering pint sleeves without a belt, USA shipping is $7.00 for any quantity.
 No problem if you have a deluxe BELTMAN leather PINT SLEEVE (or two!!) Convert your standard 16oz. (pint) bar glass into a great-looking mug with a handle and experience old-world nostalgia of class and luxury with a heavy-duty BULLHIDE or HORSE HIDE leather pint sleeve.
They are made from the same sturdy leather that is used in our belts, and are border-stitched, black-edged, waxed, and lock-screwed together. They should last through many years of serious beer (or iced tea) drinking. This is a BELTMAN original design that you will not find anywhere else.
We will stamp them with our BELTMAN logo or other fun images at no charge. Bullhide pint sleeves are available in natural, brown or black; or NATURAL horse hide (which mellows nicely with age). They make great gifts too! Matching coasters: $3.00 each.
Glass NOT included! If you are interested in the pint sleeve, you probably already have your own pint glass collection anyway!
|


# coding=utf-8
"""
module containing brownian motion model related classes
"""
from json import loads
from engine import Producer
# classical producer
[docs]class MultiProducer(Producer):
def __init__(self, *producers):
"""
initializer
:param list(Producer) or produces: list of producers to be used one after another
"""
super(MultiProducer, self).__init__()
#: list(Producer): list of consumers to be used one after another
self.producers = list()
for p in producers:
if isinstance(p, (tuple, list)):
self.producers.extend(p)
else:
self.producers.append(p)
for p in self.producers:
if isinstance(p, (tuple, list)):
for pp in p:
assert isinstance(pp, Producer)
else:
assert isinstance(p, Producer)
self.initial_state = [p.initial_state for p in self.producers]
[docs] def initialize(self, grid, num_of_paths, seed):
""" inits producer for a simulation run """
for p in self.producers:
p.initialize(grid, num_of_paths, seed)
self.grid = grid
self.num_of_paths = num_of_paths
self.seed = seed
# self.initial_state.date = grid[0]
[docs] def initialize_worker(self, process_num=None):
""" inits producer for a simulation run on a single process """
for p in self.producers:
p.initialize_worker(process_num)
# self.initial_state.process = process_num
self.random.seed(hash(self.seed) + hash(process_num))
[docs] def initialize_path(self, path_num=None):
""" inits producer for next path, i.e. sets current state to initial state"""
for p in self.producers:
p.initialize_path(path_num)
# self.state = copy(self.initial_state)
# self.state.path = path_num
self.random.seed(hash(self.seed) + hash(path_num))
[docs] def evolve(self, new_date):
"""
evolve to the new process state at the next date, i.e. do one step in the simulation
:param date new_date: date of the new state
:return State:
"""
self.state = [p.evolve(new_date) for p in self.producers]
return self.state
[docs]class DeterministicProducer(Producer):
def __init__(self, sample_list, func=None, initial_state=None):
func = (lambda s, i: sample_list[s.path][i])
super(DeterministicProducer, self).__init__(func, initial_state)
self.grid = range(len(sample_list[0]))
self.num_of_paths = len(sample_list)
[docs] def evolve(self, new_date):
return super(DeterministicProducer, self).evolve(self.grid.index(new_date))
[docs]class StringReaderProducer(DeterministicProducer):
def __init__(self, data_str, str_decoder=None):
if str_decoder is None:
str_decoder = loads
data = str_decoder(data_str)
super(StringReaderProducer, self).__init__(data)


Welcome to luknator coding quiz session! You have 5 minutes to complete all 5 questions! Leave your email for the prize!
Which ice cream flavor do you like?
Vanilla
Chocolate
Cookies
Rum
What is HTML?
A strucutre
Conent
Headings, meta info
All of above
What you do after work?
Reading
Sleeping
Outing
Sporting
Why do you use Boostrap?
Easy
short learning curve
Fun
All of above
Which company do you work for?
Netflix
Shopify
Congradulations! Claim your quiz gift at HR!


- [2023] 1 Paper accepted in IEEE Transactions of Image Processing on Salient Object Detection. 📃
- [2023] 1 Paper accepted in CVIU on Interactive Neural Painting. 📃
- [2023] Got promoted to Senior Applied Scientist 🚀
- [2022] 1 Paper accepted in CVPR on video super resolution 📃


Additional validation rules for XML instances including Physical Process components
Req 46
There shall be one and only one "gml:identifier" for any PhysicalSystem. (Req 46)
Req 46
The value of the "codespace" attribute of a "gml:identifier" must be "uniqueID". (Req 46)


Mnml Calendar
This design is in response to an incredibly well designed new iOS calendar app called Minimal Cal. It's simple, modern, and cuts away a lot of the fluff that you don't really need. Right now, they only have a mobile version, but in imagining what a web app would look like, I designed this mockup. While this is my design, it is inspired completely by the real Minimal Cal app and I have no affiliation with them.
Role
Designer
Project Type
Web App, Calendar
Working Prototype
Previous
Waltz Vineyards


This is Timothy Zhao's personal website. He recently graduated from UC Berkeley with a degree in Electrical Engineering and Computer Science.
About the guy
Originally from Ohio, he likes architecture, memes, and table tennis. Likes to think of himself as amiable and values humility. Some pillars of Tim's life are to adapt, stay positive, and persist. Hopes to one day figure out life.


Hello, I'm Shubham Khandalkar.
I'm a full-stack web developer.
ABOUT
Who's this Guy?
I am a Full Stack Web Developer with experience of 3 Years.
I have been enjoying coding for the last 10 Years.!!
I have passion for solving real world problems.
I have been enjoying coding for the last 10 Years.!!
I have passion for solving real world problems.
PROJECTS
CONTACT
Have a question or want to work together?
Email me at<EMAIL_ADDRESS>You can also contact me at<PHONE_NUMBER>