Skip to content

Commit d96b20f

Browse files
ana-pantilieana-pantilie
authored
kore-repl: represent Remaining states correctly (#2335)
1 parent 3d10ab9 commit d96b20f

File tree

9 files changed

+163
-53
lines changed

9 files changed

+163
-53
lines changed

‎kore/src/Kore/Reachability/ClaimState.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module Kore.Reachability.ClaimState
77
, extractUnproven
88
, extractStuck
99
, retractRewritable, isRewritable
10+
, isRemaining
1011
, ClaimState (..)
1112
, claimState
1213
, ClaimStateTransformer (..)
@@ -101,6 +102,9 @@ retractRewritable _ = Nothing
101102
isRewritable :: ClaimState a -> Bool
102103
isRewritable = isJust . retractRewritable
103104

105+
isRemaining :: ClaimState a -> Bool
106+
isRemaining = isJust . extractRemaining
107+
104108
data ClaimStateTransformer a val =
105109
ClaimStateTransformer
106110
{ claimedTransformer :: a -> val

‎kore/src/Kore/Repl.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Copyright : (c) Runtime Verification, 2019
55
License : NCSA
66
Maintainer : [email protected]
77
-}
8+
{-# LANGUAGE Strict #-}
89

910
module Kore.Repl
1011
( runRepl

‎kore/src/Kore/Repl/Data.hs

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Copyright : (c) Runtime Verification, 2019
55
License : NCSA
66
Maintainer : [email protected]
77
-}
8+
{-# LANGUAGE Strict #-}
89

910
module Kore.Repl.Data
1011
( ReplCommand (..)
@@ -43,6 +44,7 @@ module Kore.Repl.Data
4344
, debugApplyEquationTransformer
4445
, debugEquationTransformer
4546
, entriesForHelp
47+
, TryApplyRuleResult (..)
4648
) where
4749

4850
import Prelude.Kore
@@ -475,8 +477,11 @@ helpText =
475477
<> entriesForHelp
476478
<>
477479
"\n\
478-
\(*) If an edge is labeled as Simpl/RD it means that the target node\n\
479-
\ was reached using either the SMT solver or the Remove Destination step.\n\
480+
\(*) If an edge is labeled CheckImplication it means that during that step\n\
481+
\ the prover detected that the claim was either proven or that it could not be\
482+
\ rewritten any further (stuck).\n\
483+
\ When the application of a rewrite rule results in a remainder and no other\
484+
\ rewrite rules apply, then the edge pointing to the remaining state is labeled Remaining.\n\
480485
\ A green node represents the proof has completed on\
481486
\ that respective branch. \n\
482487
\ A red node represents a stuck configuration.\n\
@@ -697,3 +702,10 @@ runUnifierWithExplanation (UnifierWithExplanation unifier) =
697702
(makeAuxReplOutput "No explanation given")
698703
(getFirst explanation)
699704
r : rs -> Right (r :| rs)
705+
706+
data TryApplyRuleResult
707+
= DoesNotApply
708+
| GetsProven
709+
| OneResult ReplNode
710+
| MultipleResults
711+
deriving (Show, Eq)

‎kore/src/Kore/Repl/Interpreter.hs

Lines changed: 36 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Copyright : (c) Runtime Verification, 2019
55
License : NCSA
66
Maintainer : [email protected]
77
-}
8+
{-# LANGUAGE Strict #-}
89

910
module Kore.Repl.Interpreter
1011
( replInterpreter
@@ -192,6 +193,7 @@ import Kore.Reachability
192193
, isTrusted
193194
, makeTrusted
194195
)
196+
import qualified Kore.Reachability.ClaimState as ClaimState
195197
import Kore.Repl.Data
196198
import Kore.Repl.Parser
197199
import Kore.Repl.State
@@ -992,17 +994,18 @@ tryAxiomClaimWorker mode ref = do
992994
-> ReplM m ()
993995
tryForceAxiomOrClaim axiomOrClaim node = do
994996
(graph, result) <-
995-
runStepper'
996-
(either mempty pure axiomOrClaim)
997-
(either pure mempty axiomOrClaim)
998-
node
997+
tryApplyAxiomOrClaim axiomOrClaim node
999998
case result of
1000-
NoResult ->
999+
DoesNotApply ->
10011000
showUnificationFailure axiomOrClaim node
1002-
SingleResult nextNode -> do
1001+
GetsProven -> do
1002+
updateExecutionGraph graph
1003+
putStrLn'
1004+
"The proof was proven without applying any rewrite rules."
1005+
OneResult nextNode -> do
10031006
updateExecutionGraph graph
10041007
field @"node" .= nextNode
1005-
BranchResult _ ->
1008+
MultipleResults ->
10061009
updateExecutionGraph graph
10071010

10081011
runUnifier'
@@ -1333,15 +1336,14 @@ unparseClaimStateComponent transformation omitList =
13331336
claimState ClaimStateTransformer
13341337
{ claimedTransformer =
13351338
makeKoreReplOutput . unparseComponent
1336-
, remainingTransformer = \goal ->
1337-
makeAuxReplOutput "Stuck: \n"
1338-
<> makeKoreReplOutput (unparseComponent goal)
1339+
, remainingTransformer =
1340+
makeKoreReplOutput . unparseComponent
13391341
, rewrittenTransformer =
13401342
makeKoreReplOutput . unparseComponent
13411343
, stuckTransformer = \goal ->
13421344
makeAuxReplOutput "Stuck: \n"
13431345
<> makeKoreReplOutput (unparseComponent goal)
1344-
, provenValue = makeAuxReplOutput "Reached bottom"
1346+
, provenValue = makeAuxReplOutput "Proven."
13451347
}
13461348
where
13471349
unparseComponent =
@@ -1386,9 +1388,10 @@ showDotGraph
13861388
=> From axiom RuleIndex
13871389
=> Gr CommonClaimState (Maybe (Seq axiom))
13881390
-> IO ()
1389-
showDotGraph =
1391+
showDotGraph gr =
13901392
flip Graph.runGraphvizCanvas' Graph.Xlib
1391-
. Graph.graphToDot graphParams
1393+
. Graph.graphToDot (graphParams gr)
1394+
$ gr
13921395

13931396
saveDotGraph
13941397
:: From axiom AttrLabel.Label
@@ -1405,32 +1408,32 @@ saveDotGraph gr format file =
14051408
void
14061409
$ Graph.addExtension
14071410
(Graph.runGraphviz
1408-
(Graph.graphToDot graphParams gr)
1411+
(Graph.graphToDot (graphParams gr) gr)
14091412
)
14101413
format
14111414
path
14121415

14131416
graphParams
14141417
:: From axiom AttrLabel.Label
14151418
=> From axiom RuleIndex
1416-
=> Graph.GraphvizParams
1419+
=> Gr CommonClaimState (Maybe (Seq axiom))
1420+
-> Graph.GraphvizParams
14171421
Graph.Node
14181422
CommonClaimState
14191423
(Maybe (Seq axiom))
14201424
()
14211425
CommonClaimState
1422-
graphParams = Graph.nonClusteredParams
1423-
{ Graph.fmtEdge = \(_, _, l) ->
1424-
[ Graph.textLabel (maybe "" ruleIndex l)
1426+
graphParams gr = Graph.nonClusteredParams
1427+
{ Graph.fmtEdge = \(_, resN, l) ->
1428+
[ Graph.textLabel (maybe "" (ruleIndex resN) l)
14251429
, Graph.Attr.Style [dottedOrSolidEdge l]
14261430
]
14271431
, Graph.fmtNode = \(_, ps) ->
14281432
[ Graph.Attr.Color
14291433
$ case ps of
14301434
Proven -> toColorList green
14311435
Stuck _ -> toColorList red
1432-
Remaining _ -> toColorList red
1433-
_ -> []
1436+
_ -> []
14341437
]
14351438
}
14361439
where
@@ -1439,14 +1442,22 @@ graphParams = Graph.nonClusteredParams
14391442
(Graph.Attr.SItem Graph.Attr.Dotted mempty)
14401443
(const $ Graph.Attr.SItem Graph.Attr.Solid mempty)
14411444
lbl
1442-
ruleIndex lbl =
1443-
case headMay . toList $ lbl of
1444-
Nothing -> "Simpl/RD"
1445-
Just rule ->
1446-
Text.Lazy.pack (showRuleIdentifier rule)
1445+
ruleIndex resultNode lbl =
1446+
let appliedRule = lbl & toList & headMay
1447+
labelWithoutRule
1448+
| isRemaining resultNode = "Remaining"
1449+
| otherwise = "CheckImplication"
1450+
in
1451+
maybe
1452+
labelWithoutRule
1453+
(Text.Lazy.pack . showRuleIdentifier)
1454+
appliedRule
14471455
toColorList col = [Graph.Attr.WC col (Just 1.0)]
14481456
green = Graph.Attr.RGB 0 200 0
14491457
red = Graph.Attr.RGB 200 0 0
1458+
isRemaining n =
1459+
let (_, _, state, _) = Graph.context gr n
1460+
in ClaimState.isRemaining state
14501461

14511462
showAliasError :: AliasError -> String
14521463
showAliasError =

‎kore/src/Kore/Repl/Parser.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Copyright : (c) Runtime Verification, 219
55
License : NCSA
66
Maintainer : [email protected]
77
-}
8+
{-# LANGUAGE Strict #-}
89

910
module Kore.Repl.Parser
1011
( commandParser

‎kore/src/Kore/Repl/State.hs

Lines changed: 73 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Copyright : (c) Runtime Verification, 2019
55
License : NCSA
66
Maintainer : [email protected]
77
-}
8+
{-# LANGUAGE Strict #-}
89

910
module Kore.Repl.State
1011
( emptyExecutionGraph
@@ -18,7 +19,7 @@ module Kore.Repl.State
1819
, smoothOutGraph
1920
, getInterestingBranchingNode
2021
, getClaimStateAt, getRuleFor, getLabels, setLabels
21-
, runStepper, runStepper'
22+
, runStepper, runStepper', tryApplyAxiomOrClaim
2223
, runUnifier
2324
, updateInnerGraph, updateExecutionGraph
2425
, addOrUpdateAlias, findAlias, substituteAlias
@@ -514,21 +515,66 @@ runStepper'
514515
-> [Axiom]
515516
-> ReplNode
516517
-> t m (ExecutionGraph, StepResult)
517-
runStepper' claims axioms node = do
518+
runStepper' claims axioms node =
519+
runStepperWorker claims axioms node
520+
& (fmap . fmap) processResult
521+
where
522+
processResult [] = NoResult
523+
processResult [(claimState', nextNode)] =
524+
case claimState' of
525+
Proven -> NoResult
526+
Stuck _ -> NoResult
527+
_ -> SingleResult . ReplNode $ nextNode
528+
processResult (fmap snd -> nextNodes) =
529+
BranchResult $ fmap ReplNode nextNodes
530+
531+
tryApplyAxiomOrClaim
532+
:: MonadState ReplState (t m)
533+
=> MonadReader (Config m) (t m)
534+
=> Monad.Trans.MonadTrans t
535+
=> MonadSimplify m
536+
=> MonadIO m
537+
=> Either Axiom SomeClaim
538+
-> ReplNode
539+
-> t m (ExecutionGraph, TryApplyRuleResult)
540+
tryApplyAxiomOrClaim axiomOrClaim node =
541+
runStepperWorker
542+
(either mempty pure axiomOrClaim)
543+
(either pure mempty axiomOrClaim)
544+
node
545+
& (fmap . fmap) processResult
546+
where
547+
processResult [] = DoesNotApply
548+
processResult [(claimState', nextNode)] =
549+
case claimState' of
550+
Proven -> GetsProven
551+
Stuck _ -> DoesNotApply
552+
Remaining _ -> DoesNotApply
553+
_ -> OneResult . ReplNode $ nextNode
554+
processResult _ = MultipleResults
555+
556+
type SuccessorNodes = [(CommonClaimState, Graph.Node)]
557+
558+
runStepperWorker
559+
:: MonadState ReplState (t m)
560+
=> MonadReader (Config m) (t m)
561+
=> Monad.Trans.MonadTrans t
562+
=> MonadSimplify m
563+
=> MonadIO m
564+
=> [SomeClaim]
565+
-> [Axiom]
566+
-> ReplNode
567+
-> t m (ExecutionGraph, SuccessorNodes)
568+
runStepperWorker claims axioms node = do
518569
stepper <- asks stepper
519570
mvar <- asks logger
520571
gph <- getExecutionGraph
521572
gr@Strategy.ExecutionGraph { graph = innerGraph } <-
522573
liftSimplifierWithLogger mvar $ stepper claims axioms gph node
523-
pure . (,) gr
524-
$ case Graph.suc innerGraph (unReplNode node) of
525-
[] -> NoResult
526-
[single] ->
527-
case getNodeState innerGraph single of
528-
Nothing -> NoResult
529-
Just (StuckNode, _) -> NoResult
530-
_ -> SingleResult . ReplNode $ single
531-
nodes -> BranchResult $ fmap ReplNode nodes
574+
let succesorNodes =
575+
getClaimState innerGraph
576+
<$> Graph.suc innerGraph (unReplNode node)
577+
return (gr, succesorNodes)
532578

533579
runUnifier
534580
:: MonadState ReplState (t m)
@@ -549,17 +595,22 @@ runUnifier sideCondition first second = do
549595

550596
getNodeState :: InnerGraph -> Graph.Node -> Maybe (NodeState, Graph.Node)
551597
getNodeState graph node =
552-
fmap (\nodeState -> (nodeState, node))
553-
. claimState ClaimStateTransformer
554-
{ claimedTransformer = const . Just $ UnevaluatedNode
555-
, remainingTransformer = const . Just $ StuckNode
556-
, rewrittenTransformer = const . Just $ UnevaluatedNode
557-
, stuckTransformer = const . Just $ StuckNode
558-
, provenValue = Nothing
559-
}
560-
. Graph.lab'
561-
. Graph.context graph
562-
$ node
598+
let (claimState', _) = getClaimState graph node
599+
nodeState =
600+
claimState ClaimStateTransformer
601+
{ claimedTransformer = const . Just $ UnevaluatedNode
602+
, remainingTransformer = const . Just $ UnevaluatedNode
603+
, rewrittenTransformer = const . Just $ UnevaluatedNode
604+
, stuckTransformer = const . Just $ StuckNode
605+
, provenValue = Nothing
606+
}
607+
claimState'
608+
in fmap (\state -> (state, node)) nodeState
609+
610+
getClaimState :: InnerGraph -> Graph.Node -> (CommonClaimState, Graph.Node)
611+
getClaimState graph node =
612+
let claimState' = node & Graph.context graph & Graph.lab'
613+
in (claimState', node)
563614

564615
nodeToGoal
565616
:: InnerGraph

‎kore/test/Test/Kore/Repl/Graph.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
{-# LANGUAGE Strict #-}
2+
13
module Test.Kore.Repl.Graph
24
( test_graph
35
) where

0 commit comments

Comments
 (0)