Skip to content

Commit

Permalink
Merge remote-tracking branch 'upstream/develop' into develop
Browse files Browse the repository at this point in the history
  • Loading branch information
@jdreier
jdreier committed Oct 8, 2019
2 parents fbde116 + 23c9eef commit 836d7eb
Show file tree
Hide file tree
Showing 31 changed files with 609 additions and 104 deletions.
6 changes: 3 additions & 3 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ ccs15-case-studies: $(CCS15_TARGETS)
grep "verified\|falsified\|processing time" case-studies/ccs15/*.spthy


REGRESSION_OBSEQ_CASE_STUDIES=issue223.spthy issue198-1.spthy issue198-2.spthy
REGRESSION_OBSEQ_CASE_STUDIES=issue223.spthy issue198-1.spthy issue198-2.spthy issue324.spthy issue331.spthy
REGRESSION_OBSEQ_TARGETS=$(subst .spthy,_analyzed-diff.spthy,$(addprefix case-studies/regression/diff/,$(REGRESSION_OBSEQ_CASE_STUDIES)))

TESTOBSEQ_CASE_STUDIES=AxiomDiffTest1.spthy AxiomDiffTest2.spthy AxiomDiffTest3.spthy AxiomDiffTest4.spthy N5N6DiffTest.spthy
Expand Down Expand Up @@ -349,7 +349,7 @@ regression-case-studies: $(REGRESSION_TARGETS) $(SEQDFS_TARGETS)
# FAST <=> processing time less than 10sec on Robert's current computer (per file)

SAPIC_CASE_STUDIES_FAST=basic/no-replication.spthy basic/replication.spthy basic/channels1.spthy basic/channels2.spthy basic/channels3.spthy basic/design-choices.spthy basic/exclusive-secrets.spthy basic/reliable-channel.spthy \
basic/let-blocks2.spthy basic/let-blocks3.spthy \
feature-let-bindings/let-blocks2.spthy feature-let-bindings/let-blocks3.spthy feature-let-bindings/match_new.spthy \
statVerifLeftRight/stateverif_left_right.spthy \
MoedersheimWebService/set-abstr.spthy MoedersheimWebService/set-abstr-lookup.spthy \
fairexchange-mini/mini10.spthy fairexchange-mini/mini2.spthy fairexchange-mini/mini4.spthy fairexchange-mini/mini6.spthy fairexchange-mini/mini8.spthy fairexchange-mini/ndc-nested-2.spthy fairexchange-mini/ndc-nested-4.spthy fairexchange-mini/ndc-nested.spthy fairexchange-mini/mini1.spthy fairexchange-mini/mini3.spthy fairexchange-mini/mini5.spthy fairexchange-mini/mini7.spthy fairexchange-mini/mini9.spthy fairexchange-mini/ndc-nested-3.spthy fairexchange-mini/ndc-nested-5.spthy fairexchange-mini/ndc-two-replications.spthy\
Expand All @@ -358,7 +358,7 @@ feature-xor/CH07.spthy feature-xor/CRxor.spthy feature-xor/KCL07.spthy \
feature-secret-channel/secret-channel.spthy \
GJM-contract/contract.spthy
# not working because of missing support for predicates
# basic/running-example.spthy basic/let-blocks.spthy
# basic/running-example.spthy feature-let-bindings/let-blocks.spthy
# encWrapDecUnwrap/encwrapdecunwrap.spthy NOTE: might be not working for other reasons as well, it was commented out investigate
# Yubikey/Yubikey.spthy NOTE commented out previously need to verify
# PKCS11/pkcs11-templates.spthy PKCS11/pkcs11-dynamic-policy.spthy \ NOTE commented out previously need to verify
Expand Down
34 changes: 16 additions & 18 deletions case-studies-regression/regression/diff/issue198-1_analyzed-diff.spthy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,14 +110,14 @@ next
step( simplify )
step( solve( AgSt_H1v( $H, $D, vote ) ▶₀ #i ) )
case Setup
MIRRORED
by sorry // Cannot prove
qed
next
case RHS
step( simplify )
step( solve( AgSt_H1v( $H, $D, vote ) ▶₀ #i ) )
case Setup
MIRRORED
by sorry // Cannot prove
qed
qed
next
Expand All @@ -143,7 +143,7 @@ next
case shuffleVoters_case_1
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
next
case shuffleVoters_case_2
Expand All @@ -167,7 +167,7 @@ next
case shuffleVoters_case_1
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
next
case shuffleVoters_case_2
Expand All @@ -186,7 +186,7 @@ next
case shuffleVoters_case_2
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
qed
next
Expand All @@ -210,7 +210,7 @@ next
case shuffleVoters_case_2
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
qed
next
Expand Down Expand Up @@ -243,11 +243,11 @@ next
backward-search
case LHS
step( simplify )
MIRRORED
by sorry // Cannot prove
next
case RHS
step( simplify )
MIRRORED
by sorry // Cannot prove
qed
next
case Rule_shuffleVoters
Expand All @@ -256,20 +256,20 @@ next
step( simplify )
step( solve( ShuffleAgents( (x+y) ) ▶₀ #i ) )
case Setup_case_1
MIRRORED
by sorry // Cannot prove
next
case Setup_case_2
MIRRORED
by sorry // Cannot prove
qed
next
case RHS
step( simplify )
step( solve( ShuffleAgents( (x+y) ) ▶₀ #i ) )
case Setup_case_1
MIRRORED
by sorry // Cannot prove
next
case Setup_case_2
MIRRORED
by sorry // Cannot prove
qed
qed
qed
Expand All @@ -279,8 +279,6 @@ end
maude tool: 'maude'
checking version: 2.7.1. OK.
checking installation: OK.
SAPIC tool: 'sapic'
Checking availablity ... OK.


analyzing: examples/regression/diff/issue198-1.spthy
Expand All @@ -289,8 +287,8 @@ analyzing: examples/regression/diff/issue198-1.spthy
analyzed: examples/regression/diff/issue198-1.spthy

output: examples/regression/diff/issue198-1.spthy.tmp
processing time: 1.469272s
DiffLemma: Observational_equivalence : verified (84 steps)
processing time: 0.474487853s
DiffLemma: Observational_equivalence : analysis incomplete (84 steps)

------------------------------------------------------------------------------

Expand All @@ -300,8 +298,8 @@ summary of summaries:
analyzed: examples/regression/diff/issue198-1.spthy

output: examples/regression/diff/issue198-1.spthy.tmp
processing time: 1.469272s
DiffLemma: Observational_equivalence : verified (84 steps)
processing time: 0.474487853s
DiffLemma: Observational_equivalence : analysis incomplete (84 steps)

==============================================================================
*/
34 changes: 16 additions & 18 deletions case-studies-regression/regression/diff/issue198-2_analyzed-diff.spthy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,14 +110,14 @@ next
step( simplify )
step( solve( AgSt_H1v( $H, $D, vote ) ▶₀ #i ) )
case Setup
MIRRORED
by sorry // Cannot prove
qed
next
case RHS
step( simplify )
step( solve( AgSt_H1v( $H, $D, vote ) ▶₀ #i ) )
case Setup
MIRRORED
by sorry // Cannot prove
qed
qed
next
Expand All @@ -143,7 +143,7 @@ next
case shuffleVoters_case_1
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
next
case shuffleVoters_case_2
Expand All @@ -167,7 +167,7 @@ next
case shuffleVoters_case_1
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
next
case shuffleVoters_case_2
Expand All @@ -186,7 +186,7 @@ next
case shuffleVoters_case_2
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
qed
next
Expand All @@ -210,7 +210,7 @@ next
case shuffleVoters_case_2
step( solve( Channel( $Hvoter, vote ) ▶₂ #i ) )
case H_vote
MIRRORED
by sorry // Cannot prove
qed
qed
next
Expand Down Expand Up @@ -243,11 +243,11 @@ next
backward-search
case LHS
step( simplify )
MIRRORED
by sorry // Cannot prove
next
case RHS
step( simplify )
MIRRORED
by sorry // Cannot prove
qed
next
case Rule_shuffleVoters
Expand All @@ -256,20 +256,20 @@ next
step( simplify )
step( solve( ShuffleAgents( (x+y) ) ▶₀ #i ) )
case Setup_case_1
MIRRORED
by sorry // Cannot prove
next
case Setup_case_2
MIRRORED
by sorry // Cannot prove
qed
next
case RHS
step( simplify )
step( solve( ShuffleAgents( (x+y) ) ▶₀ #i ) )
case Setup_case_1
MIRRORED
by sorry // Cannot prove
next
case Setup_case_2
MIRRORED
by sorry // Cannot prove
qed
qed
qed
Expand All @@ -279,8 +279,6 @@ end
maude tool: 'maude'
checking version: 2.7.1. OK.
checking installation: OK.
SAPIC tool: 'sapic'
Checking availablity ... OK.


analyzing: examples/regression/diff/issue198-2.spthy
Expand All @@ -289,8 +287,8 @@ analyzing: examples/regression/diff/issue198-2.spthy
analyzed: examples/regression/diff/issue198-2.spthy

output: examples/regression/diff/issue198-2.spthy.tmp
processing time: 1.207189s
DiffLemma: Observational_equivalence : verified (84 steps)
processing time: 1.075869959s
DiffLemma: Observational_equivalence : analysis incomplete (84 steps)

------------------------------------------------------------------------------

Expand All @@ -300,8 +298,8 @@ summary of summaries:
analyzed: examples/regression/diff/issue198-2.spthy

output: examples/regression/diff/issue198-2.spthy.tmp
processing time: 1.207189s
DiffLemma: Observational_equivalence : verified (84 steps)
processing time: 1.075869959s
DiffLemma: Observational_equivalence : analysis incomplete (84 steps)

==============================================================================
*/
Loading

0 comments on commit 836d7eb

Please sign in to comment.