massive simplifications

case-studies-regression/fast-tests/features/configuration/configuration_analyzed.spthy

@@ -5,21 +5,14 @@ theory TestConfiguration begin
 functions: fst/1, pair/2, snd/1
 equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
-text{* the abstract state after partial evaluation contains 3 facts:
 
-1. F1( ~x )
 
-2. Fr( ~z )
 
-3. In( z )
 
-This abstract state results in 1 refined multiset rewriting rules.
-Note that the original number of multiset rewriting rules was 1.
-
-*}
+configuration: "--auto-sources --stop-on-trace=BFS"
 
 rule (modulo E) Testing:
-   [ Fr( ~x ) ] --[ Test( ~x ) ]-> [ F1( ~x ) ]
+   [ Fr( x ) ] --[ Test( x ) ]-> [ F1( x ) ]
 
   /* has exactly the trivial AC variant */
 
@@ -32,35 +25,34 @@ guarded formula characterizing all satisfying traces:
 simplify
 SOLVED // trace found
 
-/* All well-formedness checks were successful. */
 
-end
-/* Output
-maude tool: 'maude'
- checking version: 2.7.1. OK.
- checking installation: OK.
-SAPIC tool: 'sapic'
-Checking availablity ... OK.
 
 
-analyzing: examples/features//configuration/configuration.spthy
 
-------------------------------------------------------------------------------
-analyzed: examples/features//configuration/configuration.spthy
 
-  output:          case-studies/temp-analysis.spthy
-  processing time: 0.042054s
-  test_lemma (exists-trace): verified (2 steps)
 
-------------------------------------------------------------------------------
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.2
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/features//configuration/configuration.spthy
 
-  output:          case-studies/temp-analysis.spthy
-  processing time: 0.042054s
+  output:          examples/features//configuration/configuration.spthy.tmp
+  processing time: 0.03s
+
   test_lemma (exists-trace): verified (2 steps)
 
 ==============================================================================

case-studies-regression/fast-tests/regression/trace/defaultoracle_analyzed-deforacle.spthy

@@ -2,17 +2,19 @@ theory DefaultOracle begin
 
 // Function signature and definition of the equational theory E
 
-functions: fst/1[destructor], pair/2, snd/1[destructor]
+functions: fst/1, pair/2, snd/1
 equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
-heuristic: o ""
+
+
+heuristic: o "" s o "" p o ""
 
 rule (modulo E) Rule:
    [ ] --[ A( ) ]-> [ ]
 
   /* has exactly the trivial AC variant */
 
-lemma Test1 [heuristic=o ""]:
+lemma Test1 [heuristic=s o "" i o "" o ""]:
   exists-trace "∃ #i. A( ) @ #i"
 /*
 guarded formula characterizing all satisfying traces:
@@ -30,21 +32,34 @@ guarded formula characterizing all satisfying traces:
 simplify
 SOLVED // trace found
 
+
+
+
+
+
+
 /* All wellformedness checks were successful. */
 
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.2
+*/
+
 end
 /* Output
 maude tool: 'maude'
- checking version: 3.2.1. OK.
+ checking version: 3.2.2. OK.
  checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: defaultoracle.spthy
 
-  processing time: 0.027392253s
-
+  output:          defaultoracle.spthy.tmp
+  processing time: 0.22s
+
   Test1 (exists-trace): verified (2 steps)
   Test2 (exists-trace): verified (2 steps)
 

case-studies-regression/features/configuration/configuration_analyzed.spthy

@@ -5,21 +5,14 @@ theory TestConfiguration begin
 functions: fst/1, pair/2, snd/1
 equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
-text{* the abstract state after partial evaluation contains 3 facts:
 
-1. F1( ~x )
 
-2. Fr( ~z )
 
-3. In( z )
 
-This abstract state results in 1 refined multiset rewriting rules.
-Note that the original number of multiset rewriting rules was 1.
-
-*}
+configuration: "--auto-sources --stop-on-trace=BFS"
 
 rule (modulo E) Testing:
-   [ Fr( ~x ) ] --[ Test( ~x ) ]-> [ F1( ~x ) ]
+   [ Fr( x ) ] --[ Test( x ) ]-> [ F1( x ) ]
 
   /* has exactly the trivial AC variant */
 
@@ -32,35 +25,34 @@ guarded formula characterizing all satisfying traces:
 simplify
 SOLVED // trace found
 
-/* All well-formedness checks were successful. */
 
-end
-/* Output
-maude tool: 'maude'
- checking version: 2.7.1. OK.
- checking installation: OK.
-SAPIC tool: 'sapic'
-Checking availablity ... OK.
 
 
-analyzing: examples/features//configuration/configuration.spthy
 
-------------------------------------------------------------------------------
-analyzed: examples/features//configuration/configuration.spthy
 
-  output:          case-studies/temp-analysis.spthy
-  processing time: 0.042054s
-  test_lemma (exists-trace): verified (2 steps)
 
-------------------------------------------------------------------------------
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.2
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/features//configuration/configuration.spthy
 
-  output:          case-studies/temp-analysis.spthy
-  processing time: 0.042054s
+  output:          examples/features//configuration/configuration.spthy.tmp
+  processing time: 0.03s
+
   test_lemma (exists-trace): verified (2 steps)
 
 ==============================================================================

examples/regression/trace/defaultoracle.spthy

@@ -1,11 +1,11 @@
 theory DefaultOracle
 begin
 
-heuristic: o
+/*heuristic: osopo*/
 rule Rule:
   []--[A()]->[]
 
-lemma Test1 [heuristic=o]:
+lemma Test1 [heuristic=soioo]:
   exists-trace
   " Ex #i. A()@i"
 

lib/theory/src/ClosedTheory.hs

@@ -116,10 +116,10 @@ getProofContext l thy = ProofContext
 
     -- Heuristic specified for the lemma > globally specified heuristic > default heuristic
     specifiedHeuristic = case lattr of
+        Just lh -> Just lh
         Nothing  -> case L.get thyHeuristic thy of
                     [] -> Nothing
-                    gh -> Just . Heuristic $ map (defaultOracleName (L.get thyInFile thy)) gh
-        lh -> defaultOracleNames lh (L.get thyInFile thy)
+                    gh -> Just (Heuristic gh)
       where
         lattr = (headMay [Heuristic gr
                     | LemmaHeuristic gr <- L.get lAttributes l])
@@ -173,10 +173,10 @@ getProofContextDiff s l thy = case s of
       | otherwise                                                        = AvoidInduction
     -- Heuristic specified for the lemma > globally specified heuristic > default heuristic
     specifiedHeuristic = case lattr of
+        Just lh -> Just lh
         Nothing  -> case L.get diffThyHeuristic thy of
                     [] -> Nothing
-                    gh -> Just . Heuristic $ map (defaultOracleName (L.get diffThyInFile thy)) gh
-        lh -> defaultOracleNames lh (L.get diffThyInFile thy)
+                    gh -> Just (Heuristic gh)
       where
         lattr = (headMay [Heuristic gr
                     | LemmaHeuristic gr <- L.get lAttributes l])
@@ -238,10 +238,10 @@ getDiffProofContext l thy = DiffProofContext (proofContext LHS) (proofContext RH
             (any isConstantRule $ filter isDestrRule $ intruderRules $ L.get (crcRules . diffThyCacheRight) thy)
 
     specifiedHeuristic = case lattr of
+        Just lh -> Just lh
         Nothing  -> case L.get diffThyHeuristic thy of
                     [] -> Nothing
-                    gh -> Just . Heuristic $ map (defaultOracleName (L.get diffThyInFile thy)) gh
-        lh -> defaultOracleNames lh (L.get diffThyInFile thy)
+                    gh -> Just (Heuristic gh)
       where
         lattr = (headMay [Heuristic gr
                     | LemmaHeuristic gr <- L.get lDiffAttributes l])

lib/theory/src/OpenTheory.hs

@@ -94,7 +94,7 @@ addAutoSourcesLemmaDiff hnd lemmaName crcLeft crcRight items =
         f (DiffRuleItem r)               = Just (DiffRuleItem r)
         f (DiffLemmaItem l)              = Just (DiffLemmaItem l)
         f (DiffTextItem t)               = Just (DiffTextItem t)
-        f (DiffConfigBlockItem b) = Just (DiffConfigBlockItem b)
+        f (DiffConfigBlockItem b)        = Just (DiffConfigBlockItem b)
         f _                              = Nothing
 
     lhsPart = if containsPartialDeconstructions crcLeft
@@ -120,7 +120,7 @@ addAutoSourcesLemmaDiff hnd lemmaName crcLeft crcRight items =
     toSide RHS (LemmaItem l)            = Just $ EitherLemmaItem (RHS, addRightLemma l)
     toSide s (RestrictionItem r)        = Just $ EitherRestrictionItem (s, r)
     toSide _ (TextItem t)               = Just $ DiffTextItem t
-    toSide _ (ConfigBlockItem b) = Just $ DiffConfigBlockItem b
+    toSide _ (ConfigBlockItem b)        = Just $ DiffConfigBlockItem b
     -- FIXME: We currently ignore predicates and sapic stuff as they should not
     --        be generated by addAutoSourcesLemma
     toSide _ (PredicateItem _)   = Nothing
@@ -397,11 +397,11 @@ defaultOption = Option False False False False False False False S.empty [] 10 5
 
 -- | Default theory
 defaultOpenTheory :: Bool -> OpenTheory
-defaultOpenTheory flag = Theory "default" [] [] (emptySignaturePure flag) [] [] defaultOption
+defaultOpenTheory flag = Theory "default" "default" [] [] (emptySignaturePure flag) [] [] defaultOption
 
 -- | Default diff theory
 defaultOpenDiffTheory :: Bool -> OpenDiffTheory
-defaultOpenDiffTheory flag = DiffTheory "default" [] [] (emptySignaturePure flag) [] [] [] [] [] defaultOption
+defaultOpenDiffTheory flag = DiffTheory "default" "default" [] [] (emptySignaturePure flag) [] [] [] [] [] defaultOption
 
 -- Add the default Diff lemma to an Open Diff Theory
 addDefaultDiffLemma:: OpenDiffTheory -> OpenDiffTheory