be.ac.umons.jsonvalidation.graph

Class KeyGraph<L>

java.lang.Object

be.ac.umons.jsonvalidation.graph.KeyGraph<L>

Type Parameters:

L - Location type

public class KeyGraph<L>
extends Object

A key graph is a directed graph constructed from ReachabilityRelation for a 1-SEVPA recognizing JSON documents.

The nodes of the graph are triplets (p, k, q) such that, from the location p, it is possible to reach the location q by reading a word k v with v a well-matched word. That is, the triplets store the fact that there is a key-value pair that can go from p to q.

There is an edge going from (q, k, q') to (p, k', p') if and only if there is an internal transition reading the comma symbol from the location q' to the location p'.

Once created, it is guaranteed that the graph is never modified.

If the 1-SEVPA is correctly built, the key graph is acyclic and, on every path in the graph, each key is seen at most once. However, it may happen that the graph contains a cycle or a path on which the same key is seen twice (typically, if the learning process is stopped before obtaining a valid hypothesis). This implementation correctly handles this case, i.e., it is guaranteed that all the algorithms eventually stop even if the graph is not "correct".

The class also maintains a list giving the nodes containing the initial location of the VPA to mark the paths' start points, and two maps:

• One giving, for all k, the nodes (s, k, s').
• One giving, for all k, the locations s such that (s, k, s') is a node.

Author:

Gaëtan Staquet

Constructor Summary

Constructors

Constructor and Description
KeyGraph(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> automaton, ReachabilityRelation<L> reachabilityRelation, OnAcceptingPathRelation<L> onAcceptingPathRelation, boolean checkGraph) Constructs the key graph using the VPA, its ReachabilityRelation, and its OnAcceptingPathRelation.

Method Summary

Modifier and Type	Method and Description
Set<L>	getLocationsReadingKey(JSONSymbol key) Gets all the locations for which there exists an internal transition reading the given key.
Set<L>	getLocationsWithReturnTransitionOnUnmarkedPathsWithAllKeysSeen(Set<JSONSymbol> seenKeys, Collection<L> locationsBeforeCall, Collection<NodeInGraph<L>> rejectedNodes) Gets all the locations in the VPA such that it is possible to read a closing curly brace and there is a path in the graph such that none of its node is marked as rejected and all the keys seen while processing the input are exactly seen on the path.
List<NodeInGraph<L>>	getNodesForKey(JSONSymbol key) Gets all the nodes that can read the given key.
net.automatalib.words.Word<JSONSymbol>	getWitnessInvalid() If the graph is invalid, provides a witness.
static <L> KeyGraph<L>	graphFor(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> automaton, boolean checkGraph) Constructs the key graph for the provided automaton.
boolean	isValid() Whether the graph does not contain a path where the same key is seen multiple times.
int	size() The size of the key graph, i.e., the number of vertices.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

KeyGraph

public KeyGraph(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> automaton,
                ReachabilityRelation<L> reachabilityRelation,
                OnAcceptingPathRelation<L> onAcceptingPathRelation,
                boolean checkGraph)

Constructs the key graph using the VPA, its ReachabilityRelation, and its OnAcceptingPathRelation.

Parameters:

automaton - The 1-SEVPA

reachabilityRelation - Its reachability relation

onAcceptingPathRelation - Its relation that indicates whether a location is on an accepting path

checkGraph - If true, checks that the graph does not contain a path where a key is seen multiple times

See Also:

graphFor(OneSEVPA, boolean)

Method Detail

graphFor

public static <L> KeyGraph<L> graphFor(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> automaton,
                                       boolean checkGraph)

Constructs the key graph for the provided automaton.

This function computes the reachability relation of the VPA.

Since the key graph may contain paths where one key is seen twice, it is possible to check that the graph is actually valid. If that check must be performed, witnesses of the reachability relation are computed.

Type Parameters:

L - Location type

Parameters:

automaton - The 1-SEVPA

checkGraph - Whether to check that the graph is valid, i.e., there is no path on which we can see the same key twice.

Returns:

The key graph

isValid

public boolean isValid()

Whether the graph does not contain a path where the same key is seen multiple times.

Returns:

True if and only if the graph does not contain a path where the same key is seen multiple times

getWitnessInvalid

public net.automatalib.words.Word<JSONSymbol> getWitnessInvalid()

If the graph is invalid, provides a witness.

Returns:

A witness that the key graph is invalid

size

public int size()

The size of the key graph, i.e., the number of vertices.

Returns:

The number of vertices

getNodesForKey

public List<NodeInGraph<L>> getNodesForKey(JSONSymbol key)

Gets all the nodes that can read the given key.

Parameters:

key - The key

Returns:

A list with the nodes

getLocationsReadingKey

public Set<L> getLocationsReadingKey(JSONSymbol key)

Gets all the locations for which there exists an internal transition reading the given key.

Parameters:

key - The key

Returns:

getLocationsWithReturnTransitionOnUnmarkedPathsWithAllKeysSeen

public Set<L> getLocationsWithReturnTransitionOnUnmarkedPathsWithAllKeysSeen(Set<JSONSymbol> seenKeys,
                                                                             Collection<L> locationsBeforeCall,
                                                                             Collection<NodeInGraph<L>> rejectedNodes)

Gets all the locations in the VPA such that it is possible to read a closing curly brace and there is a path in the graph such that none of its node is marked as rejected and all the keys seen while processing the input are exactly seen on the path. This allows to know the set of locations that are actually reached in the VPA after reading the current object and from which we can read a closing curly brace.

Parameters:

seenKeys - The set of keys seen while reading the input

locationsBeforeCall - The locations of the VPA before reading the opening curly brace that opened the current object

rejectedNodes - A collection of nodes in the graph that are marked as rejected

Returns:

The set of locations from which the VPA can read the closing curly brace