configuration: Replace Set of <goal>s with list. Only first goal is a…

…ctive
kframework · Apr 20, 2020 · cfdf1aa · cfdf1aa
1 parent 4eab015
commit cfdf1aa
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 17 deletions.
diff --git a/prover/drivers/base.md b/prover/drivers/base.md
@@ -1,13 +1,13 @@
 Configuration
 =============
 
-The configuration consists of a assoc-commutative bag of goals. Only goals
-marked `<active>` are executed to control the non-determinism in the system. The
-`<k>` cell contains the Matching Logic Pattern for which we are searching for a
-proof. The `<strategy>` cell contains an imperative language that controls which
-(high-level) proof rules are used to complete the goal. The `<trace>` cell
-stores a log of the strategies used in the search of a proof and other debug
-information. Eventually, this could be used for constructing a proof object.
+The configuration consists of a list of goals. The first goal is considered
+active. The `<k>` cell contains the Matching Logic Pattern for which we are
+searching for a proof. The `<strategy>` cell contains an imperative language
+that controls which (high-level) proof rules are used to complete the goal. The
+`<trace>` cell stores a log of the strategies used in the search of a proof and
+other debug information. Eventually, this could be used for constructing a proof
+object.
 
 ```k
 module PROVER-CONFIGURATION
@@ -23,8 +23,7 @@ module PROVER-CONFIGURATION
       <prover>
         <exit-code exit=""> 1 </exit-code>
         <goals>
-          <goal multiplicity="*" type="Set" format="%1%i%n%2, %3, %4%n%5%n%6%n%7%n%8%n%d%9">
-            <active format="active: %2"> true:Bool </active>
+          <goal multiplicity="*" type="List" format="%1%i%n%3, %3%n%4%n%65n%6%n%7%n%d%8">
             <id format="id: %2"> .K </id>
             <parent format="parent: %2"> .K </parent>
             <k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>

diff --git a/prover/strategies/core.md b/prover/strategies/core.md
@@ -89,18 +89,16 @@ completed, its result is replaced in the parent goal and the subgoal is removed.
 ```k
   syntax Strategy ::= goalStrat(GoalId)
   rule <prover>
-         <goal> <id> PID </id>
-                <active> _ => true </active>
-                <strategy> goalStrat(ID) => RStrat ... </strategy>
-                ...
-         </goal>
          ( <goal> <id> ID </id>
-                  <active> true:Bool </active>
                   <parent> PID </parent>
                   <strategy> RStrat:TerminalStrategy </strategy>
                   ...
            </goal> => .Bag
          )
+         <goal> <id> PID </id>
+                <strategy> goalStrat(ID) => RStrat ... </strategy>
+                ...
+         </goal>
          ...
        </prover>
 ```
@@ -116,7 +114,6 @@ Proving a goal may involve proving other subgoals:
          ( .Bag =>
              <goal>
                <id> ID:Int </id>
-               <active> true </active>
                <parent> PARENT </parent>
                <strategy> SUBSTRAT </strategy>
                <k> SUBGOAL </k>
@@ -127,7 +124,6 @@ Proving a goal may involve proving other subgoals:
          )
          <goal>
            <id> PARENT </id>
-           <active> true => false </active>
            <strategy> subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID:Int) ... </strategy>
            <local-context> LC::Bag </local-context>
            <trace> TRACE </trace>