> ## Documentation Index > Fetch the complete documentation index at: https://docs.state.space/llms.txt > Use this file to discover all available pages before exploring further. # ERC20: Validate the Pausable Feature > Sandbox tutorial ## Get Started Welcome to the introduction tutorial on how to use State Space. This tutorial is based on the OpenZeppelin ERC20 implementation and the [Pausable](https://docs.openzeppelin.com/contracts/2.x/api/lifecycle) feature. Read the test objective below, and follow the steps to understand how State Space works. **Objective:** Determine who should be able to `mint()` tokens after the contract has been paused. [Login](https://state.space/login) or create your account [here](https://state.space/sign-up) From the "Home" menu, [open](https://state.space/me) the pre-loaded ERC20 Workbench project. You will see a folder tree containing the ERC20 project and a canvas with a pre-designed transaction sequence. **Expand** the folder tree to view all the externally visable functions as components. These components can be dragged onto the canvas to create multi-contract test scenarios and transaction sequences (e.g. end-to-end flows, integration tests, etc). There are four types of components: Blue = `CALL` - function call\ Purple = `VIEW` - view function\ Green = `CREATE` - constructor\ Gray = `DEPLOY` - a deployment script *** ### The transaction sequence Since the objective is to determine whether any EOA can mint tokens *after* the contract has been paused, we created a sequence of transactions that calls first deploys the contract, and then calls `pause()` and `mint()` in succession: `Deployment` → `constructor(...)` → `pause(...)` → `mint(...)` It should look like this: You can use your existing deployment scripts (if you have one in Foundry or Hardhat) to create custom deployment nodes for deeper testing. ### Configure symbolic input parameters State Space supports the use of both symbolic and concrete input values, or any combination thereof for both transaction values and function parameters. For values set to symbolic, State Space will automatically search for and generate [structured dynamic inputs](/docs/overview/concepts#structured-dynamic-inputs) that will satisfy the conditions of the entire transaction sequence. What if we're not sure what parameters to set? Rather than manually figuring out all combinations to test, we can use symbolic values to explore all possible inputs for any field. Let's assume that Alice is the contract deployer and `Bob` is the `initialOwner`. In our test setup, we configure the following: * Set the transaction `From` field for the `constructor()` function call to `Alice`. * Set the `initialOwner` parameter in the `constructor()` to `Bob`. * Leave the transaction `From` field for `pause()` set to symbolic to consider all EOAs preconfigured in the deployment (`Alice` and `Bob`). So far, it should look like this: Since part of our objective is to determine whether any externally owned account (EOA) can successfully mint tokens, we take a symbolic approach for the `mint()` transaction: * We leave the transaction `From` field for `mint()` set to symbolic. Symbolic means it represents all possible EOAs (limited to the accounts configured in the deployment) rather than being fixed to a specific account (a concrete input). This allows State Space to autonomously discover which accounts can trigger unique execution paths. * We also leave the function parameters of `mint()` symbolic (`to` and `amount`), allowing State Space to explore all possible input values to determine which concrete inputs and conditions (if any) would result in a successful mint operation after `pause` has been called. It should look like this: This hybrid symbolic/concrete input parameterization ensures that we can still maximize coverage while minimizing state space explosion. Alternatively, you could set everything to symbolic too, and you'll get a wider state space to explore and analyze. It will just take more compute time, and include scenarios that may not be as meaningful in answering the test objective. Now, it's time to explore the state space. *** Select the icon to start exploring and generating the execution state space. State Space will autonomously explore code paths, automatically taking into consideration all multi-contract interactions for your test scenario. For each unique code path it discovers, it will generate the verified concrete input conditions that trigger their execution. Because State Space models the *full EVM semantics*, the symbolic execution can reason about every operation with bit level precision, uncover obscure edge cases manual testing misses, and maximize coverage and path exploration. Discovered execution paths, input conditions, and resulting contract state, will appear dynamically during execution. Once completed, detailed coverage metrics will be displayed for each run. The results should display 14 test cases (execution paths) and 46% health coverage. Run times can vary depending on the number of sequences, transaction depth, the amount of symbolic parameters, compute, and more. Complex codebases will require increased allocation of compute resources. If you're curious about what performance to expect, [reach out to us](mail:contact@state.space) and we'll help you estimate it. Feel free to experiement with different sequences to analyze different behaviors. *** As you review the results, you’ll notice that every execution path results in a revert, with no successful `mint()` transaction occurring. We determine that we could not find any path or combination of inputs that will successfully lead to a mint transaction, and provide the test cases for each executed path. This outcome matches our expectations because after invoking the `pause()` function, the `_paused` contract value should be set to `true` preventing any minting operation from successfully completing. Let's confirm that the `_paused` state value was indeed updated, and visually validate all other states and state changes are correct. **Select** and **open** the test case (execution path) with the following input conditions: * `Alice` deploys the contract and `Bob` is set as the `initialOwner` * `Bob` calls the `pause()` function * Transaction reverts with an `EnforcedPause` error after `Bob` attempts to mint `1` token to `Alice`. Once you have opened test case, click through the `constructor()` --> `pause()` --> `mint()` transactions. You can examine the storage layout, values, changes, account balances, and emitted events that occurred throughout the execution of the transaction sequence. Locate the `_paused` storage value, and validate it was correctly set to `true` after the `pause()` transaction and that it remained unchanged after the `mint()` transaction (which reverted). Source code is also highlighted for lines and branch coverage: export From the same view, select your test framework (Hardhat or Foundry) to copy or download the complete test case. You can also include emitted events in the test case by selecting the "Export Test" button in the top left of the screen. The test case represents the exact behavior of code, including both expected and unexpected behavior. Return to the canvas, and delete the `pause` function from the transaction sequence, and reconnect the `mint(..)` function to the `constructor()`. Run the analysis again. You'll see the `mint(..)` transaction completing successfully. Select a path where a successful `mint` operation occurs, and analyze the contract state and changes. Find the `_totalSupply` state value, and evaluate its behavior. Has `_totalSupply` increased as expected by the `amount`? Have the balances correctly updated as well? Toggle through the transactions to become familiar with the process. If you would like a tutorial on any specific topic, of have suggestions on improving existing tutorials, please [contact us](mail:contact@state.space)! We'd love to hear from you.